Is it possible to install coq-hammer via nix?
It seems that it isn't available at nix.
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.
I can go ahead and add the new releases
I had a go here but I might have bitten off more than I can chew
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.
We should probably request help from the maintainer (or Karl).
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?
No. To install coq-hammer via opam, this requires installing coq via opam first.
But if you do not care too much about the Coq version, you could use the
coqPackages_8_15 version which is alread available.
Oh.. Thanks! Hadn't understood that it was available on the older coq version.
Ali, you should open an issue upstream: their build system is crap, as you said.
This line for instance:
at least at one point, the Dune build worked (but has to be separate for
I can fix/patch it if it doesn't
Why have both a makefile based build and a dune build?
Also it seems the repo doesn't even have a working CI atm.
If I had the time I would do the following:
in that order.
@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
in fact, it's what I recommend to all Coq-community projects currently
OK whatever they are I am currently writing a patch to fix the dune build here at least
@Karl Palmskog What is the reason for the separate coq-hammer-tacitcs and coq-hammer packages?
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
one should never depend on
coq-hammer in a project where one has applied the hammer, but always only on
the main reason is that ATP runs are not reproducible generally
OK i've fixed the dune build https://github.com/lukaszcz/coqhammer/pull/157
You don't need to use the makefile at all anymore
It should correctly install those c,c++ binaries
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