split FinFun and Permutation into List and Vector

[andres-erbsen]

Fixes / closes #????

• Added changelog.
• Added / updated documentation.

• Opened overlay pull requests.
  • remove PermutationCompat mit-plv/fiat-crypto#2091
  • Require Arith before using hintdb arith rocq-community/corn#215
  • Require Import FinFun before using it adampetcher/fcf#49
  • https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/617

[andres-erbsen]

@proux01 can you help me understand what this CI error means? (I have an overlay that I'd like to test).

building '/nix/store/kazrhh85jndwbaz7ijw3yqd82g2r6m4v-rocq-core9.0-corn-dev.drv'...
Running phase: unpackPhase
unpacking source archive /nix/store/2i68d6p7r699zh5s00ddw3841i4f8n2i-source
source root is source
Running phase: patchPhase
Running phase: updateAutotoolsGnuConfigScriptsPhase
Running phase: configurePhase
no configure script, doing nothing
Running phase: buildPhase
no Makefile or custom buildPhase, doing nothing
Running phase: installPhase
no Makefile or custom installPhase, doing nothing
Running phase: fixupPhase
error: builder for '/nix/store/kazrhh85jndwbaz7ijw3yqd82g2r6m4v-rocq-core9.0-corn-dev.drv' failed to produce output path for output 'out' at '/nix/store/kazrhh85jndwbaz7ijw3yqd82g2r6m4v-rocq-core9.0-corn-dev.drv.chroot/root/nix/store/d1cycii872xznn3f515dcakh869di1rh-rocq-core9.0-corn-dev'
Error: Process completed with exit code 1.

[andres-erbsen]

Dear coq-nix-toolbox maintainers, @CohenCyril @Zimmi48: Can you (easily) help me tell what the CI is complaining about here? See overlay declaration, code. Thanks!

[proux01]

Sorry for the delayed answer. The message seems to tell that corn didn't compile/install anything. We should try to understand why (maybe they recently modified something in their build system?).

[proux01]

Indeed the lines

Running phase: configurePhase
no configure script, doing nothing

should be something like (c.f. for instance https://github.com/rocq-prover/stdlib/actions/runs/15546209619/job/43768830203 )

Running phase: configurePhase
patching script interpreter paths in ./configure.sh
./configure.sh: interpreter directive changed from "#!/usr/bin/env sh" to "/nix/store/xg75pc4yyfd5n2fimhb98ps910q5lm5n-bash-5.2p37/bin/sh"
configure flags: ''

But not sure what's happening since your overlay branch still contains the configure.sh file?

[proux01]

Ok, I think I found it, could you try moving this line up 6 lines above (just below the comment) so that it is in coq-common-bundles and not in common-bundles

[proux01]

(common-bundles applies to both coq and rocq, and since there is no corn in rocq, strange things happen if we add an empty package there)

[andres-erbsen]

fiat-crypto says Makefile:27: etc/coq-scripts/Makefile.vo_closure: No such file or directory

[proux01]

IIRC (check in .nix/coq-overlays/fiat-crypto) putting an overlay in any other repo than the main one disactivates all the git submodule churn, so you may need to add overlays for those dependencies or something like that.

[andres-erbsen]

Thank you! I don't understand why the behavior arises or how it makes sense, but sure seems to work as you advised.