| Message ID | 20211116175936.11987-1-zimon.toutoune@gmail.com |
|---|---|
| State | Accepted |
| Headers | show |
| Series | [bug#51896] gnu: Add coq-semantics. | expand |
| Context | Check | Description |
|---|---|---|
| cbaines/comparison | success | View comparision |
| cbaines/git branch | success | View Git branch |
| cbaines/applying patch | success | View Laminar job |
| cbaines/issue | success | View issue |
Le 16 novembre 2021 12:59:36 GMT-05:00, zimoun <zimon.toutoune@gmail.com> a écrit : >* 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"? >+ #: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? >+ (("-libs nums") "-use-ocamlfind -pkg num -libs num")))) Should this instead be in a snippet in the origin record? >+ (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? >+ (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
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? Cheers, simon
Le 16 novembre 2021 13:13:56 GMT-05:00, zimoun <zimon.toutoune@gmail.com> a écrit : >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 :) > >Cheers, >simon
Pushed v2 to master as 2d60af4d6d486591c5a6981659d1771b7c69781a to 7537ec816ffe0aaa6677c53604ac12fe9d9ca250. Thanks!
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")