search

coq-community / coq-nix-toolbox

Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
MIT License
32 stars 9 forks source link

Add MenhirLib & use it in CompCert #249

Closed vbgl closed 3 weeks ago

proux01 commented 3 weeks ago

@vbgl how does this relate to https://github.com/NixOS/nixpkgs/pull/331749 ?

proux01 commented 3 weeks ago

Apparently, this is more complete with older versions but my PR enabled to use ocamlPackages.menhir with dev versions. I'm updating my PR to avoid conflicts.

vbgl commented 3 weeks ago

What’s the use case for “ocamlPackages.menhir with dev versions”?

proux01 commented 3 weeks ago

CI

vbgl commented 3 weeks ago

I’m not sure to understand. In what kind of CI do you need the development version of the menhir OCaml libraries?

proux01 commented 3 weeks ago

That would for instance be needed in the CI of Coq (if it were implemented with coq-nix-toolbox), that compiles CompCert master, particularly now that CompCert depends on MenhirLib.

vbgl commented 3 weeks ago

Ok, so it’s hypothetical. And I’m truly skeptical that the development branch of CompCert starts using unreleased features of the menhir OCaml library.

proux01 commented 3 weeks ago

@vbgl you're probably right about CompCert. Unfortunately, there are also packages like coq-json that require both ocamlPackages.menhir and coqPackages.MenhirLib and they need to be the exact same version for this to work. Thus, the non overridable ocamlPackages.menhir means it's impossible to easyly overlay coqPackages.MenhirLib and even worse (since current fixed version of menhir doesn't compile on Coq master) it's impossible to test things like coq-json on Coq master.

The fix offered in https://github.com/NixOS/nixpkgs/pull/331749/files is quite trivial and is basically a copy/paste of what's done for ocamlPackages.elpi for more than two years now, so I'm pretty confident this is both working and trouble free.

vbgl commented 3 weeks ago

Thanks for the detailed explanation.