Stream: Nix toolbox devs & users

Topic: coq-hammer via nix


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 14 2023 at 10:44):

I can go ahead and add the new releases

view this post on Zulip Ali Caglayan (Apr 14 2023 at 14:40):

I had a go here but I might have bitten off more than I can chew

view this post on Zulip Ali Caglayan (Apr 14 2023 at 14:40):

https://github.com/NixOS/nixpkgs/pull/226161

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 14 2023 at 15:52):

We should probably request help from the maintainer (or Karl).

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Apr 14 2023 at 16:23):

No. To install coq-hammer via opam, this requires installing coq via opam first.

view this post on Zulip 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.

view this post on Zulip Julin S (Apr 14 2023 at 16:32):

Oh.. Thanks! Hadn't understood that it was available on the older coq version.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Apr 17 2023 at 11:29):

I can fix/patch it if it doesn't

view this post on Zulip Ali Caglayan (Apr 17 2023 at 13:04):

Why have both a makefile based build and a dune build?

view this post on Zulip Ali Caglayan (Apr 17 2023 at 13:04):

Also it seems the repo doesn't even have a working CI atm.

view this post on Zulip Ali Caglayan (Apr 17 2023 at 13:06):

If I had the time I would do the following:

  1. Write a GitHub actions workflow
  2. Move completely to the Dune based build

in that order.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 17 2023 at 13:39):

in fact, it's what I recommend to all Coq-community projects currently

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 17 2023 at 14:29):

@Karl Palmskog What is the reason for the separate coq-hammer-tacitcs and coq-hammer packages?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 17 2023 at 14:31):

the main reason is that ATP runs are not reproducible generally

view this post on Zulip Ali Caglayan (Apr 17 2023 at 15:02):

OK i've fixed the dune build https://github.com/lukaszcz/coqhammer/pull/157

view this post on Zulip Ali Caglayan (Apr 17 2023 at 15:02):

You don't need to use the makefile at all anymore

view this post on Zulip Ali Caglayan (Apr 17 2023 at 15:03):

It should correctly install those c,c++ binaries

view this post on Zulip 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: May 24 2024 at 21:01 UTC