(define-module (gnu packages rocq)
  #:use-module (gnu packages autotools)
  #:use-module (gnu packages base)  
  #:use-module (gnu packages coq)
  #:use-module (gnu packages gawk)
  #:use-module (gnu packages gtk)  
  #:use-module (gnu packages multiprecision)
  #:use-module (gnu packages ocaml)
  #:use-module (gnu packages version-control)
  #:use-module (guix build-system dune)  
  #:use-module (guix build-system gnu)
  #:use-module (guix download)
  #:use-module (guix gexp)
  #:use-module (guix git-download)  
  #:use-module (guix licenses)
  #:use-module (guix packages))


(define rocq-essential-pkgs '("rocq-core" "rocq-runtime" "coq-core"))
(define rocqide-pkg "rocqide")
(define rocqide-server-pkg "coqide-server") ;; not changed as of V9.2.0.

(define (rocq-build-phases packages-to-install)
  ;; Run "make help-install" in rocq to see instructions for "final users".
  ;; We build all final user targets, but only install a subset.
  ;; This is to allow the main language, the IDE and the IDE server to be
  ;; installed separately.
  (let ((all-packages
	 `(,@rocq-essential-pkgs ,rocqide-pkg ,rocqide-server-pkg)))
    #~(modify-phases %standard-phases
	(add-before 'build 'configure
          (lambda* (#:key outputs #:allow-other-keys)
            (let* ((out (assoc-ref outputs "out"))
                   (rocqlib (string-append out "/lib/ocaml/site-lib/rocq/")))
              (invoke "./configure" "-prefix" out
                      "-libdir" rocqlib))))
	(add-before 'build 'make-dunestrap
          (lambda _ (invoke "make" "dunestrap")))
	(replace 'build
	  (lambda _ (invoke "dune" "build" "-p"
			    (string-join '#$all-packages ","))))
	(replace 'check
	  (lambda _ (invoke "dune" "build" "@check")))
	(replace 'install
	  (lambda* (#:key outputs #:allow-other-keys)
	    (let* ((out (assoc-ref outputs "out"))
		   (libdir (string-append out "/lib/ocaml/site-lib")))
	      (primitive-eval
	       (cons* invoke "dune" "install"
		      "--prefix" out '#$packages-to-install))))))))

(define-public rocq
  (package
    (name "rocq")
    (version "9.2.0")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/rocq-prover/rocq.git")
             (commit (string-append "V" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32
         "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
    (native-search-paths
     (list (search-path-specification
            (variable "ROCQPATH")
            (files (list "lib/rocq/user-contrib")))))
    (build-system dune-build-system)
    (arguments
     (list
      #:phases
      (rocq-build-phases rocq-essential-pkgs)))
    (propagated-inputs
     (list ocaml-zarith camlzip ocaml-lablgtk3-sourceview3 ocaml-yojson))
    (inputs
     (list gmp))
    (native-inputs
     (list ocaml-ounit2 which))
    (properties '((upstream-name . "rocq"))) ; also for inherited packages
    (home-page "https://rocq-prover.org/")
    (synopsis "Proof assistant for higher-order logic")
    (description
     "The Rocq Prover is an interactive theorem prover, or proof assistant. 
It provides a formal language to write mathematical definitions, executable 
algorithms and theorems together with an environment for semi-interactive 
development of machine-checked proofs.")
    ;; The source code is distributed under lgpl2.1.
    ;; Some of the documentation is distributed under opl1.0+.
    (license (list lgpl2.1 opl1.0+))))

(define-public rocqide-server
  (package
    (inherit rocq)
    (name "rocqide-server")
    (arguments
     (list
      #:phases (rocq-build-phases `(,rocqide-server-pkg))))))

(define-public rocqide
  (package
    (inherit rocq)
    (name "rocqide")
    (arguments
     (list
      #:phases (rocq-build-phases `(,rocqide-pkg))))))

(define-public lambda
  (package
    (name "lambda")
    (version "0.0.1")
    (source (origin
	      (method git-fetch)
	      (uri (git-reference
		     (url "git://git.rostovtsev.org/lambda")
		     (commit "v0.0.1")))
	      (sha256
	       (base32 ;; nix32
		"0yk1shd3d6kz8pdbv11fg462kcvxvsw6lvmp7plqiiqicm4fbir4"))))
    (build-system gnu-build-system)
    (native-inputs (list coq
			 autoconf
			 automake   ; alocal used here for some reason
			 which	    ; used in autoconf step
			 gawk	    ; used in autoconf step
			 ))
    (synopsis "Fundamental objects and results in the untyped lambda calculus.")
    (description
     (string-append
      "A Rocq library for working with a weak call-by-value lambda calculus."
      "Provides proofs of the Church-Rosser Properties and Uniform Confluence."))
    (home-page "https://git.rostovtsev.org/lambda")
    (license gpl3+)))