[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
?
Your comment

This issue is archived.

To comment on this conversation send an email to 51896@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 51896
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch