Julin S (Apr 14 2023 at 09:01): Julin S (Apr 14 2023 at 09:01):Is it possible to install coq-hammer via nix?
It seems that it isn't available at nix.
Théo Zimmermann (Apr 14 2023 at 09:10):It is available, just not in the default package set: https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/coqhammer/default.nix. Since there actually are releases for Coq 8.16 and 8.17, this is just a matter of updating the derivation to include those.
Ali Caglayan (Apr 14 2023 at 10:44):I can go ahead and add the new releases
Ali Caglayan (Apr 14 2023 at 14:40):I had a go here but I might have bitten off more than I can chew
Ali Caglayan (Apr 14 2023 at 14:40):https://github.com/NixOS/nixpkgs/pull/226161
Ali Caglayan (Apr 14 2023 at 14:45):However just bumping the version doesn't work
nix-repl> :b coqPackages_8_17.coqhammer
error: builder for '/nix/store/4q7mjxd4l7812hwggvsdbzdvazzws0f6-coq8.17-coqhammer-1.3.2-coq8.17.drv' fa
iled with exit code 1;
last 6 log lines:
> unpacking sources
> unpacking source archive /nix/store/720lb7dm2fvxn6n0qh4dkz0y0p3z2fmc-source
> source root is source
> patching sources
> substitute(): ERROR: file 'Makefile.coq.local' does not exist
> /nix/store/5s1yg5l36wzgy1dj0vv1ibarc4g7vrdr-stdenv-linux/setup: line 136: pop_var_context: hea
d of shell_variables not a function context
For full logs, run 'nix log /nix/store/4q7mjxd4l7812hwggvsdbzdvazzws0f6-coq8.17-coqhammer-1.3.2-
coq8.17.drv'.
it's a bit of a PITA that coqhammer uses this Makefile.coq.local crap. My attempt above was just to port it to build with Dune but it looks like the makefile stuff is needed. Not sure what to do.
Théo Zimmermann (Apr 14 2023 at 15:52):We should probably request help from the maintainer (or Karl).
Julin S (Apr 14 2023 at 16:16):I got coq installed via nix. Would it be possible to use opam to install coq-hammer and make it work with the nix-installed coq?
Théo Zimmermann (Apr 14 2023 at 16:23):No. To install coq-hammer via opam, this requires installing coq via opam first.
Théo Zimmermann (Apr 14 2023 at 16:23):But if you do not care too much about the Coq version, you could use the coqPackages_8_15 version which is alread available.
Julin S (Apr 14 2023 at 16:32):Oh.. Thanks! Hadn't understood that it was available on the older coq version.
Vincent Laporte (Apr 17 2023 at 11:28):Ali, you should open an issue upstream: their build system is crap, as you said.
This line for instance:
https://github.com/lukaszcz/coqhammer/blob/v1.3.2+8.17/Makefile#L8
Karl Palmskog (Apr 17 2023 at 11:29):at least at one point, the Dune build worked (but has to be separate for coq-hammer-tactics and coq-hammer)
Karl Palmskog (Apr 17 2023 at 11:29):I can fix/patch it if it doesn't
Ali Caglayan (Apr 17 2023 at 13:04):Why have both a makefile based build and a dune build?
Ali Caglayan (Apr 17 2023 at 13:04):Also it seems the repo doesn't even have a working CI atm.
Ali Caglayan (Apr 17 2023 at 13:06):If I had the time I would do the following:
in that order.
Karl Palmskog (Apr 17 2023 at 13:39):@Ali Caglayan there are many reasons to both have a coq_makefile and Dune build, and makes the project more resilient to build system changes
Karl Palmskog (Apr 17 2023 at 13:39):in fact, it's what I recommend to all Coq-community projects currently
Ali Caglayan (Apr 17 2023 at 13:40):OK whatever they are I am currently writing a patch to fix the dune build here at least
Ali Caglayan (Apr 17 2023 at 14:29):@Karl Palmskog What is the reason for the separate coq-hammer-tacitcs and coq-hammer packages?
Karl Palmskog (Apr 17 2023 at 14:30):coq-hammer depends on a bunch of external tools and is the full hammer system. coq-hammer-tactics are standalone general FOL-like automation tactics for Coq that happen to be useful for hammer proof reconstruction
Karl Palmskog (Apr 17 2023 at 14:31):one should never depend on coq-hammer in a project where one has applied the hammer, but always only on coq-hammer-tactics
Karl Palmskog (Apr 17 2023 at 14:31):the main reason is that ATP runs are not reproducible generally
Ali Caglayan (Apr 17 2023 at 15:02):OK i've fixed the dune build https://github.com/lukaszcz/coqhammer/pull/157
Ali Caglayan (Apr 17 2023 at 15:02):You don't need to use the makefile at all anymore
Ali Caglayan (Apr 17 2023 at 15:03):It should correctly install those c,c++ binaries
Théo Zimmermann (Apr 18 2023 at 17:39):FWIW, coq-hammer-tactics is available in the Coq Platform on all OSes, but coq-hammer is not available on Windows.
Last updated: Nov 29 2023 at 21:01 UTC