[PATCH] gnu: Add coq-semantics.

  • Done
  • quality assurance status badge
Details
2 participants
  • Julien Lepiller
  • zimoun
Owner
unassigned
Submitted by
zimoun
Severity
normal
Z
Z
zimoun wrote on 16 Nov 2021 18:59
(address . guix-patches@gnu.org)(name . zimoun)(address . zimon.toutoune@gmail.com)
20211116175936.11987-1-zimon.toutoune@gmail.com
* gnu/packages/coq.scm (coq-semantics): New variable.
---
gnu/packages/coq.scm | 54 ++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 54 insertions(+)

Toggle diff (76 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index dccb9bea4c..ca9335302f 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -7,6 +7,7 @@
;;; Copyright © 2020 raingloom <raingloom@riseup.net>
;;; Copyright © 2020 Robin Green <greenrd@greenrd.org>
;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
+;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -573,6 +574,59 @@ (define-public coq-equations
kernel.")
(license license:lgpl2.1)))
+(define-public coq-semantics
+ (package
+ (name "coq-semantics")
+ (version "8.13.0")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/coq-community/semantics")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(("coq" ,coq)
+ ("ocaml" ,ocaml)
+ ("ocamlbuild" ,ocamlbuild)
+ ("ocaml-findlib" ,ocaml-findlib)))
+ (inputs
+ `(("ocaml-num" ,ocaml-num)))
+ (arguments
+ `(#:tests? #f ;included in Makefile
+ #:phases
+ (modify-phases %standard-phases
+ (add-after 'unpack 'fix-ocaml-Big_int
+ (lambda _
+ (substitute* "Makefile.coq.local"
+ ;; Num has part of OCaml and now external
+ (("-libs nums") "-use-ocamlfind -pkg num -libs num"))))
+ (delete 'configure)
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (invoke "make"
+ (string-append "COQLIB=" (assoc-ref outputs "out")
+ "/lib/coq/")
+ "install"))))))
+ (home-page "https://github.com/coq-community/semantics")
+ (synopsis "Survey of semantics styles")
+ (description
+ "This package provides a survey of programming language semantics styles,
+from natural semantics through structural operational, axiomatic, and
+denotational semantics, for a miniature example of an imperative programming
+language. Their encoding, the proofs of equivalence of different styles,
+abstract interpretation, and the proof of soundess obtained from axiomatic
+semantics or abstract interpretation is done in Coq. The tools can be run
+inside Coq, thus making them available for proof by reflection. Code can also
+be extracted and connected to a yacc-based parser, thanks to the use of a
+functor parameterized by a module type of strings. A hand-written parser is
+also provided in Coq, without associated proofs.")
+ (license license:expat)))
+
(define-public coq-stdpp
(package
(name "coq-stdpp")

base-commit: 122396075f12b013b6bde56dafb895587b95bc9d
--
2.32.0
J
J
Julien Lepiller wrote on 16 Nov 2021 19:07
2F8617DF-AC9B-48BB-9DB8-868DFE4A2B8E@lepiller.eu
Le 16 novembre 2021 12:59:36 GMT-05:00, zimoun <zimon.toutoune@gmail.com> a écrit :
Toggle quote (46 lines)
>* gnu/packages/coq.scm (coq-semantics): New variable.
>---
> gnu/packages/coq.scm | 54 ++++++++++++++++++++++++++++++++++++++++++++
> 1 file changed, 54 insertions(+)
>
>diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
>index dccb9bea4c..ca9335302f 100644
>--- a/gnu/packages/coq.scm
>+++ b/gnu/packages/coq.scm
>@@ -7,6 +7,7 @@
> ;;; Copyright © 2020 raingloom <raingloom@riseup.net>
> ;;; Copyright © 2020 Robin Green <greenrd@greenrd.org>
> ;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
>+;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com>
> ;;;
> ;;; This file is part of GNU Guix.
> ;;;
>@@ -573,6 +574,59 @@ (define-public coq-equations
> kernel.")
> (license license:lgpl2.1)))
>
>+(define-public coq-semantics
>+ (package
>+ (name "coq-semantics")
>+ (version "8.13.0")
>+ (source
>+ (origin
>+ (method git-fetch)
>+ (uri (git-reference
>+ (url "https://github.com/coq-community/semantics")
>+ (commit (string-append "v" version))))
>+ (file-name (git-file-name name version))
>+ (sha256
>+ (base32
>+ "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
>+ (build-system gnu-build-system)
>+ (native-inputs
>+ `(("coq" ,coq)
>+ ("ocaml" ,ocaml)
>+ ("ocamlbuild" ,ocamlbuild)
>+ ("ocaml-findlib" ,ocaml-findlib)))
>+ (inputs
>+ `(("ocaml-num" ,ocaml-num)))
>+ (arguments
>+ `(#:tests? #f ;included in Makefile

You mean it's run at the same time as "make"?

Toggle quote (7 lines)
>+ #:phases
>+ (modify-phases %standard-phases
>+ (add-after 'unpack 'fix-ocaml-Big_int
>+ (lambda _
>+ (substitute* "Makefile.coq.local"
>+ ;; Num has part of OCaml and now external

was?

Toggle quote (2 lines)
>+ (("-libs nums") "-use-ocamlfind -pkg num -libs num"))))

Should this instead be in a snippet in the origin record?

Toggle quote (8 lines)
>+ (delete 'configure)
>+ (replace 'install
>+ (lambda* (#:key outputs #:allow-other-keys)
>+ (invoke "make"
>+ (string-append "COQLIB=" (assoc-ref outputs "out")
>+ "/lib/coq/")
>+ "install"))))))

Would it make sense to have it in #:make-flags?

Toggle quote (20 lines)
>+ (synopsis "Survey of semantics styles")
>+ (description
>+ "This package provides a survey of programming language semantics styles,
>+from natural semantics through structural operational, axiomatic, and
>+denotational semantics, for a miniature example of an imperative programming
>+language. Their encoding, the proofs of equivalence of different styles,
>+abstract interpretation, and the proof of soundess obtained from axiomatic
>+semantics or abstract interpretation is done in Coq. The tools can be run
>+inside Coq, thus making them available for proof by reflection. Code can also
>+be extracted and connected to a yacc-based parser, thanks to the use of a
>+functor parameterized by a module type of strings. A hand-written parser is
>+also provided in Coq, without associated proofs.")
>+ (license license:expat)))
>+
> (define-public coq-stdpp
> (package
> (name "coq-stdpp")
>
>base-commit: 122396075f12b013b6bde56dafb895587b95bc9d
Z
Z
zimoun wrote on 16 Nov 2021 19:13
(name . Julien Lepiller)(address . julien@lepiller.eu)
CAJ3okZ2MCs+3ja5gB+rQnBcNyR2T-rfo4M6wsEi-2Hr+nK6dDQ@mail.gmail.com
Re,

On Tue, 16 Nov 2021 at 19:07, Julien Lepiller <julien@lepiller.eu> wrote:

Toggle quote (9 lines)
> >+ (replace 'install
> >+ (lambda* (#:key outputs #:allow-other-keys)
> >+ (invoke "make"
> >+ (string-append "COQLIB=" (assoc-ref outputs "out")
> >+ "/lib/coq/")
> >+ "install"))))))
>
> Would it make sense to have it in #:make-flags?

I did the same way as other packages. That's fine to correct all the
others, WDYT?


Cheers,
simon
J
J
Julien Lepiller wrote on 16 Nov 2021 19:24
(name . zimoun)(address . zimon.toutoune@gmail.com)
77112651-00DA-44BC-923B-865919B4458D@lepiller.eu
Le 16 novembre 2021 13:13:56 GMT-05:00, zimoun <zimon.toutoune@gmail.com> a écrit :
Toggle quote (16 lines)
>Re,
>
>On Tue, 16 Nov 2021 at 19:07, Julien Lepiller <julien@lepiller.eu> wrote:
>
>> >+ (replace 'install
>> >+ (lambda* (#:key outputs #:allow-other-keys)
>> >+ (invoke "make"
>> >+ (string-append "COQLIB=" (assoc-ref outputs "out")
>> >+ "/lib/coq/")
>> >+ "install"))))))
>>
>> Would it make sense to have it in #:make-flags?
>
>I did the same way as other packages. That's fine to correct all the
>others, WDYT?

If it works yes, but in a separate patch :)

Toggle quote (3 lines)
>
>Cheers,
>simon
Z
Z
zimoun wrote on 16 Nov 2021 19:51
[PATCH v2 1/5] gnu: Add coq-semantics.
(address . 51896@debbugs.gnu.org)
20211116185154.22062-1-zimon.toutoune@gmail.com
* gnu/packages/coq.scm (coq-semantics): New variable.
---
gnu/packages/coq.scm | 51 ++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 51 insertions(+)

Toggle diff (73 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index dccb9bea4c..322bdb126e 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -7,6 +7,7 @@
;;; Copyright © 2020 raingloom <raingloom@riseup.net>
;;; Copyright © 2020 Robin Green <greenrd@greenrd.org>
;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
+;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -573,6 +574,56 @@ (define-public coq-equations
kernel.")
(license license:lgpl2.1)))
+(define-public coq-semantics
+ (package
+ (name "coq-semantics")
+ (version "8.13.0")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/coq-community/semantics")
+ (commit (string-append "v" version))))
+ (modules '((guix build utils)))
+ (snippet
+ '(substitute* "Makefile.coq.local"
+ ;; Num was part of OCaml and now external
+ (("-libs nums") "-use-ocamlfind -pkg num -libs num")))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(("coq" ,coq)
+ ("ocaml" ,ocaml)
+ ("ocamlbuild" ,ocamlbuild)
+ ("ocaml-findlib" ,ocaml-findlib)))
+ (inputs
+ `(("ocaml-num" ,ocaml-num)))
+ (arguments
+ `(#:tests? #f ;included in Makefile
+ #:make-flags (list (string-append "COQLIBINSTALL="
+ (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib"))
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'configure))))
+ (home-page "https://github.com/coq-community/semantics")
+ (synopsis "Survey of semantics styles")
+ (description
+ "This package provides a survey of programming language semantics styles,
+from natural semantics through structural operational, axiomatic, and
+denotational semantics, for a miniature example of an imperative programming
+language. Their encoding, the proofs of equivalence of different styles,
+abstract interpretation, and the proof of soundess obtained from axiomatic
+semantics or abstract interpretation is done in Coq. The tools can be run
+inside Coq, thus making them available for proof by reflection. Code can also
+be extracted and connected to a yacc-based parser, thanks to the use of a
+functor parameterized by a module type of strings. A hand-written parser is
+also provided in Coq, without associated proofs.")
+ (license license:expat)))
+
(define-public coq-stdpp
(package
(name "coq-stdpp")

base-commit: 122396075f12b013b6bde56dafb895587b95bc9d
--
2.32.0
Z
Z
zimoun wrote on 16 Nov 2021 19:51
[PATCH v2 2/5] gnu: coq-mathcomp: Adjust '#:make-flags'.
(address . 51896@debbugs.gnu.org)
20211116185154.22062-2-zimon.toutoune@gmail.com
* gnu/packages/coq.scm (coq-mathcomp)[arguments]<#:make-flags>: Set install
destination.
<#:phases>: Remove replace 'install.
---
gnu/packages/coq.scm | 11 ++++-------
1 file changed, 4 insertions(+), 7 deletions(-)

Toggle diff (28 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 322bdb126e..602a2d305d 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -326,17 +326,14 @@ (define-public coq-mathcomp
("coq" ,coq)))
(arguments
`(#:tests? #f ; No tests.
+ #:make-flags (list (string-append "COQLIBINSTALL="
+ (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib"))
#:phases
(modify-phases %standard-phases
(delete 'configure)
(add-before 'build 'chdir
- (lambda _ (chdir "mathcomp") #t))
- (replace 'install
- (lambda* (#:key outputs #:allow-other-keys)
- (invoke "make" "-f" "Makefile.coq"
- (string-append "COQLIB=" (assoc-ref outputs "out")
- "/lib/coq/")
- "install"))))))
+ (lambda _ (chdir "mathcomp") #t)))))
(home-page "https://math-comp.github.io/")
(synopsis "Mathematical Components for Coq")
(description "Mathematical Components for Coq has its origins in the formal
--
2.32.0
Z
Z
zimoun wrote on 16 Nov 2021 19:51
[PATCH v2 3/5] gnu: coq-autosubst: Adjust '#:make-flags'.
(address . 51896@debbugs.gnu.org)
20211116185154.22062-3-zimon.toutoune@gmail.com
* gnu/packages/coq.scm (coq-autosubst)[arguments]<#:make-flags>: Set install
destination.
<#:phases>: Remove replace 'install.
---
gnu/packages/coq.scm | 12 ++++--------
1 file changed, 4 insertions(+), 8 deletions(-)

Toggle diff (27 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 602a2d305d..fc739a0475 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -502,16 +502,12 @@ (define-public coq-autosubst
(build-system gnu-build-system)
(arguments
`(#:tests? #f
+ #:make-flags (list (string-append "COQLIBINSTALL="
+ (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib"))
#:phases
(modify-phases %standard-phases
- (delete 'configure)
- (replace 'install
- (lambda* (#:key outputs #:allow-other-keys)
- (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
- (invoke "make"
- (string-append "COQLIB=" (assoc-ref outputs "out")
- "/lib/coq/")
- "install"))))))
+ (delete 'configure))))
(native-inputs
`(("coq" ,coq)))
(home-page "https://www.ps.uni-saarland.de/autosubst/")
--
2.32.0
Z
Z
zimoun wrote on 16 Nov 2021 19:51
[PATCH v2 5/5] gnu: coq-stdpp: Adjust '#:make-flags'.
(address . 51896@debbugs.gnu.org)
20211116185154.22062-5-zimon.toutoune@gmail.com
* gnu/packages/coq.scm (coq-stdpp)[arguments]<#:make-flags>: Set install
destination.
<#:phases>: Remove replace 'install.
---
gnu/packages/coq.scm | 11 ++++-------
1 file changed, 4 insertions(+), 7 deletions(-)

Toggle diff (26 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index aeba0eb5da..a0579f8869 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -633,15 +633,12 @@ (define-public coq-stdpp
`(("coq" ,coq)))
(arguments
`(#:tests? #f ; Tests are executed during build phase.
+ #:make-flags (list (string-append "COQLIBINSTALL="
+ (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib"))
#:phases
(modify-phases %standard-phases
- (delete 'configure)
- (replace 'install
- (lambda* (#:key outputs #:allow-other-keys)
- (invoke "make"
- (string-append "COQLIB=" (assoc-ref outputs "out")
- "/lib/coq/")
- "install"))))))
+ (delete 'configure))))
(description "This project contains an extended \"Standard Library\" for
Coq called coq-std++. The key features are:
@itemize
--
2.32.0
Z
Z
zimoun wrote on 16 Nov 2021 19:51
[PATCH v2 4/5] gnu: coq-equations: Adjust '#:make-flags'.
(address . 51896@debbugs.gnu.org)
20211116185154.22062-4-zimon.toutoune@gmail.com
* gnu/packages/coq.scm (coq-equations)[arguments]<#:make-flags>: Set install
destination.
<#:phases>: Remove replace 'install.
---
gnu/packages/coq.scm | 11 ++++-------
1 file changed, 4 insertions(+), 7 deletions(-)

Toggle diff (28 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fc739a0475..aeba0eb5da 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -547,17 +547,14 @@ (define-public coq-equations
`(("ocaml-zarith" ,ocaml-zarith)))
(arguments
`(#:test-target "test-suite"
+ #:make-flags (list (string-append "COQLIBINSTALL="
+ (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib"))
#:phases
(modify-phases %standard-phases
(replace 'configure
(lambda* (#:key outputs #:allow-other-keys)
- (invoke "sh" "./configure.sh")))
- (replace 'install
- (lambda* (#:key outputs #:allow-other-keys)
- (invoke "make"
- (string-append "COQLIB=" (assoc-ref outputs "out")
- "/lib/coq/")
- "install"))))))
+ (invoke "sh" "./configure.sh"))))))
(home-page "https://mattam82.github.io/Coq-Equations/")
(synopsis "Function definition plugin for Coq")
(description "Equations provides a notation for writing programs
--
2.32.0
J
J
Julien Lepiller wrote on 18 Nov 2021 04:35
Re: [bug#51896] [PATCH] gnu: Add coq-semantics.
(name . zimoun)(address . zimon.toutoune@gmail.com)(address . 51896-done@debbugs.gnu.org)
20211118043512.5222b2c0@tachikoma.lepiller.eu
Pushed v2 to master as 2d60af4d6d486591c5a6981659d1771b7c69781a to
7537ec816ffe0aaa6677c53604ac12fe9d9ca250. Thanks!
Closed
?