| Message ID | 79d544f7d8ba64b631a6f0f1d2ef0b08@disroot.org |
|---|---|
| State | Accepted |
| Headers | show |
| Series | [bug#57540] Add ocaml-elpi (a dependency of coq-mathcomp-analysis) | expand |
| Context | Check | Description |
|---|---|---|
| cbaines/comparison | success | View comparision |
| cbaines/git-branch | success | View Git branch |
| cbaines/applying patch | fail | View Laminar job |
| cbaines/issue | success | View issue |
| cbaines/comparison | success | View comparision |
| cbaines/git-branch | success | View Git branch |
| cbaines/applying patch | fail | View Laminar job |
| cbaines/issue | success | View issue |
| cbaines/applying patch | fail | View Laminar job |
| cbaines/issue | success | View issue |
| cbaines/applying patch | fail | View Laminar job |
| cbaines/issue | success | View issue |
| cbaines/applying patch | fail | View Laminar job |
| cbaines/issue | success | View issue |
| cbaines/applying patch | fail | View Laminar job |
| cbaines/issue | success | View issue |
| cbaines/applying patch | fail | View Laminar job |
| cbaines/issue | success | View issue |
Hi Garek, thanks for the patches! As I understand it, these patches introduce 8 new packages, but I count only 7 (with this one which didn't make it as a part of the series). Could you split the last patch, so each new package has its own patch? Also, some points in your patches: For "Don't know about directory test", you can try with an argument: #:test-target "some-dir". This directory is the directory where tests are located. If there is no single directory, you can try #:test-target "." Descriptions should use our subset of texinfo. Basically, lists should look like: @itemize @item foo @item bar @end itemize and you can use @file, @code, etc as you see fit (to replace markdown's "`"). Whenever possible, we try not to rely on github tarballs, so it'd be best to use a git-reference in all your patches :) In coq-elpi: > + ;; Remove the useless line > + ;; "src/META.coq-elpi" > + ;; in file _CoqProject. > + ;; It does not affect > + ;; the success of compliation. should be "compilation". And then I wonder why you need that at all, if it doesn't change compilation result? > + #t)) Please don't use #t at the end of phases anymore. > + (replace 'check The gnu-build-system already runs "make test", doesn't it? Why do you need to replace this phase? In coq-mathcomp-hierarchy-builder: > + (replace 'check Instead of replacing this phase, maybe try #:test-target "test-suite" > + ;; Makefile.common has no references to tests at all > + ;; (yet). If that means that future versions will have tests (for instance if master has tests), maybe this should say it more explicitely. Once you fix all this, could you send a v2 series? Thank you!
Hi Julien, Julien Lepiller <julien@lepiller.eu> skribis: > thanks for the patches! As I understand it, these patches introduce 8 > new packages, but I count only 7 (with this one which didn't make it as > a part of the series). Could you split the last patch, so each new > package has its own patch? Could you take a look at v2 of this patch series? https://issues.guix.gnu.org/57540 TIA! Ludo’.
Le Sat, 24 Sep 2022 15:05:18 +0200, Ludovic Courtès <ludo@gnu.org> a écrit : > Hi Julien, > > Julien Lepiller <julien@lepiller.eu> skribis: > > > thanks for the patches! As I understand it, these patches introduce > > 8 new packages, but I count only 7 (with this one which didn't make > > it as a part of the series). Could you split the last patch, so > > each new package has its own patch? > > Could you take a look at v2 of this patch series? > > https://issues.guix.gnu.org/57540 > > TIA! > > Ludo’. Haha! This went under my radar. I pushed a part of this series on master as 8371ad64083970f68c8e1dd5f04b1f10d9cf029d to d46e955d93692f3c4b5387aaf709a2e5e43b57b4. These were: ocaml-ansiterminal, coq-mathcomp-{finmap,bigenough}, python-version, python-editables and python-icdiff. I made a few changes esp. to extend descriptions, remove a few comments that were unneeded. I also removed the recursive? flag for mathcomp packages since it was not needed. This already took quite a bit of time because patches were malformed (not your fault, but somehow the subject line was always incorrect) and in a seemingly random order. Also, they almost all have conflicts with current master. I'm a bit too tired to figure out the rest. Could you rebase the remaining patches on top of master? Please make sure that when applying a patch, it is possible to build the package without applying more patches. So, make sure dependencies are added before dependents. If you lack inspiration, the README is often a good place to use. A few notes on the patches: The description is often a single line, a copy of the synopsis, or missing a final point. In the description of ocaml-elpi, it says (last line): "ELPI is free software released under the terms of LGPL 2.1 or above.". No need to repeat the license here. Also, this means that the license should be lgpl2.1+, instead of plain lgpl2.1. For python packages, I see you add python to the inputs. Why is that? The python-build-system already provides python. python-hatchling should go in python-build instead of xyz. For jsonschema, please don't change the name of the package. It looks like python-jsonschema-next (4.5.1) does not have any dependent, so updating this package instead might be better than adding a new one, wdyt? Thanks!
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 0e8e5b2..59f324e 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -26,6 +26,7 @@ ;;; Copyright © 2021 Sarah Morgensen <iskarian@mgsn.dev> ;;; Copyright © 2022 Maxim Cournoyer <maxim.cournoyer@gmail.com> ;;; Copyright © 2022 John Kehayias <john.kehayias@protonmail.com> +;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org> ;;; ;;; This file is part of GNU Guix. ;;; @@ -8741,3 +8742,104 @@ (define-public ocaml-bibtex2html (description "This package allows you to produce, from a set of bibliography files in BibTeX format, a bibliography in HTML format.") (license license:gpl2))) + +(define-public ocaml-elpi + (package + (name "ocaml-elpi") + ;; For more information on which version works with Coq 8.15, + ;; see the relevant issue: + ;; https://github.com/math-comp/hierarchy-builder/issues/297 + ;; Here we use + ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 + + ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15) + ;; + ;; The package ocaml-elpi@1.16.5 appears to require a different + ;; build process. + (version "1.15.2") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/LPCIC/elpi") + (commit (string-append "v" version)) + (recursive? #t))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0swzqabwrxqb6sz8zpild2lfcnk3l0zxi9fw61dy2g1pzws2j2jy")))) + (build-system dune-build-system) + (arguments + `(;; When running phase 'check', fails with the error: + ;; Error: Don't know about directory test specified on the + ;; command line! + ;; + ;; The "make tests" command requires replacing /usr/bin/time + ;; with the location of the input package "time". + #:tests? #f)) + (propagated-inputs (list ocaml-stdlib-shims + ocaml-ppxlib + ocaml-menhir + ocaml-re + ocaml-ppx-deriving + ocaml-atdgen + ocaml-atdts + ocaml-camlp-streams + ocaml-biniou + ocaml-yojson)) + (native-inputs (list ocaml-ansiterminal ocaml-cmdliner time)) + (home-page "https://github.com/LPCIC/elpi") + (synopsis "ELPI - Embeddable λProlog Interpreter") + (description + "ELPI implements a variant of λProlog enriched with Constraint +Handling Rules, a programming language well suited to manipulate +syntax trees with binders. + +ELPI is designed to be embedded into larger applications written in +OCaml as an extension language. It comes with an API to drive the +interpreter and with an FFI for defining built-in predicates and data +types, as well as quotations and similar goodies that are handy to +adapt the language to the host application. + +This package provides both a command line interpreter (elpi) and a +library to be linked in other applications (eg by passing -package +elpi to ocamlfind). + +The ELPI programming language has the following features: + +- Native support for variable binding and substitution, via an Higher +Order Abstract Syntax (HOAS) embedding of the object language. The +programmer does not need to care about technical devices to handle +bound variables, like De Bruijn indices. + +- Native support for hypothetical context. When moving under a binder +one can attach to the bound variable extra information that is +collected when the variable gets out of scope. For example when +writing a type-checker the programmer needs not to care about managing +the typing context. + +- Native support for higher order unification variables, again via +HOAS. Unification variables of the meta-language (λProlog) can be +reused to represent the unification variables of the object language. +The programmer does not need to care about the unification-variable +assignment map and cannot assign to a unification variable a term +containing variables out of scope, or build a circular assignment. + +- Native support for syntactic constraints and their meta-level +handling rules. The generative semantics of Prolog can be disabled by +turning a goal into a syntactic constraint (suspended goal). A +syntactic constraint is resumed as soon as relevant variables gets +assigned. Syntactic constraints can be manipulated by constraint +handling rules (CHR). + +- Native support for backtracking. To ease implementation of search. + +- The constraint store is extensible. The host application can declare +non-syntactic constraints and use custom constraint solvers to check +their consistency. + +- Clauses are graftable. The user is free to extend an existing +program by inserting/removing clauses, both at runtime (using +implication) and at \"compilation\" time by accumulating files. + +ELPI is free software released under the terms of LGPL 2.1 or above.") + (license license:lgpl2.1)))