[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#64249] [PATCH ocaml-team v3 2/6] gnu: coq: Update to 8.17.1.
From: |
pukkamustard |
Subject: |
[bug#64249] [PATCH ocaml-team v3 2/6] gnu: coq: Update to 8.17.1. |
Date: |
Mon, 24 Jul 2023 14:54:05 +0000 |
Hi,
Julien Lepiller <julien@lepiller.eu> writes:
> I'm not sure why, but this is breaking all coq dependents, with
> messages similar to:
>
> cannot guess a path for Coq libraries; please use -coqlib option or
> ensure you have installed the package containing Coq's stdlib
> (coq-stdlib in OPAM) If you intend to use Coq without a standard
> library, the -boot -noinit options must be used.
>
> I think this is because coq-stdlib is mostly empty for some reason.
A couple of build failures later this is where I'm at:
- Coq 8.17.1 includes considerable changes to the build system.
- Some `dune` files are autogenerated with `make dunestrap` (which runs
the OCaml program `tools/dune_rule_gen/gen_rules.ml`.
- In the v3 patches I submitted `make dunestrap` was not being run,
resulting in missing dune files and a quite empty `coq-stdlib`
package.
- The 8.17.1 generated dune files for `coq-stdlib` reference things in
`coq-core` directly with relative paths instead of letting
dune/findlib find them (with entries in the `libraries` stanza in dune
files). This makes building `coq-core` and `coq-stdlib` seperately
more tricky.
I've asked in #coq for ideas on how `coq-stdlib` and `coq-core` can be
built seperately/kept in separate packages. Nothing yet.
What do you think about merging `coq-core`, `coq-stdlib` and `coq` into
a single package? Not as nice as the current situation, but maybe a way
to go without too many custom patches/hacks?
CC: Arnaud and Josselin who might be interested in Coq stuff.
Thanks,
pukkamustard
>> * gnu/packages/coq.scm (coq-core, coq-stdlib, coq): Update to 8.17.1
>> and remove test-target argument.
>> ---
>> gnu/packages/coq.scm | 24 +++++-------------------
>> 1 file changed, 5 insertions(+), 19 deletions(-)
>>
>> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
>> index 09ca4030ea..3332707a71 100644
>> --- a/gnu/packages/coq.scm
>> +++ b/gnu/packages/coq.scm
>> @@ -53,7 +53,7 @@ (define-module (gnu packages coq)
>> (define-public coq-core
>> (package
>> (name "coq-core")
>> - (version "8.16.1")
>> + (version "8.17.1")
>> (source
>> (origin
>> (method git-fetch)
>> @@ -63,7 +63,7 @@ (define-public coq-core
>> (file-name (git-file-name name version))
>> (sha256
>> (base32
>> - "0ljpqhh5lfsim29fcfp2xfcvm3j84pf1mb0gnpdr8vcqqw7mqwpf"))
>> + "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))
>> (patches (search-patches "coq-fix-envvars.patch"))))
>> (native-search-paths
>> (list (search-path-specification
>> @@ -83,8 +83,7 @@ (define-public coq-core
>> (native-inputs
>> (list ocaml-ounit2 which))
>> (arguments
>> - `(#:package "coq-core"
>> - #:test-target "."))
>> + `(#:package "coq-core"))
>> (properties '((upstream-name . "coq"))) ; also for inherited
>> packages (home-page "https://coq.inria.fr")
>> (synopsis "Proof assistant for higher-order logic")
>> @@ -101,19 +100,7 @@ (define-public coq-stdlib
>> (inherit coq-core)
>> (name "coq-stdlib")
>> (arguments
>> - `(#:package "coq-stdlib"
>> - #:test-target "."
>> - #:phases
>> - (modify-phases %standard-phases
>> - (add-before 'build 'fix-dune
>> - (lambda _
>> - (substitute* "user-contrib/Ltac2/dune"
>> - (("coq-core.plugins.ltac2")
>> - (string-join
>> - (map (lambda (plugin) (string-append
>> "coq-core.plugins." plugin))
>> - '("ltac2" "number_string_notation" "tauto"
>> "cc"
>> - "firstorder"))
>> - " "))))))))
>> + `(#:package "coq-stdlib"))
>> (inputs
>> (list coq-core gmp ocaml-zarith))
>> (native-inputs '())))
>> @@ -123,8 +110,7 @@ (define-public coq
>> (inherit coq-core)
>> (name "coq")
>> (arguments
>> - `(#:package "coq"
>> - #:test-target "."))
>> + `(#:package "coq"))
>> (propagated-inputs
>> (list coq-core coq-stdlib))
>> (native-inputs '())))