Remove Stdlib dependency

[proux01]

Except for a few tests, that get their own make targets.
Everything seems to work except derive.eqb for primitive integers, I don't know why but without the last commit, derive.eqb fails for option, list,... with an error message about primitive integers.

Cc @CohenCyril following mathcomp meeting this morning

• update CI to actually ensure we are not depending on stdlib
• update CI with tests (as in Coq CI, orthogonal to current PR)
• update CI with Stdlib specific tests

[gares]

Amazing work, thanks!

I have a pain points with this patch, too many .in files. I'm wondering if we can reduce the .in files by adding a single core.v.in file that contains the ifdefs for stuff that is Coq or Corelib and exports them, and then use Require Import Core.X Core.Y unconditionally.

Do you this this would work? I may even give it a try myself, but you surely have a better gut feeling about this now that you have patched the entire code base.

[proux01]

Should work, let me try

[gares]

Much better!

[proux01]

Done, CI green (but this includes #770 so #770 should probably be merged first)

[gares]

I had troubles run things on 8.20 since the dune theory Stdlib is not there, so I added a proxy, but I guess I broke 9.0 now since the proxy does not require Stdlib in the dune file.

I think you have a dune.in for that, but seems gone

[proux01]

Indeed, the few stslib specifics test didn't run anymore on 8.20. I thought it wasn't that important since they are run on 9.0 and master anyway (and we'll drop 8.20 at some point), so not worth speding time on this I'd say.

[gares]

I found the trick, I'm fixing it.

[proux01]

Note that if you retrieve Stdlib specific tests on 8.20, you may want to add the coq-elpi-tests-stdlib job to the 8.20 bundle in .nix/config.nix

[gares]

everything seems to work here on 8.20, I would not mind a "make" on 9.0 if you have the checkout at hand.

[proux01]

make on 9.0 fails (2 failed), let me fix that

[gares]

Hum, I think you added a second copy of Bool.v.in, other than that looks perfect.

[proux01]

It's not really a copy, the one in elpi.core is essentially void for >= 9.0 whereas the one in elpi_stdlib is Bool.v from Stdlib.
Note that I had to comment out the last line of apps/tc/examples/tutorial.v
I also need to squash/cleanup the git log

[gares]

Dear @Janno (and other Bluerock folks) this is a heads up that this PR is ready and will be merged soon.

It makes master work before and after the "stdlib split", on Coq 8.20 and Rocq 9.0.
It strives to break as little as possible, but I don't have your code in CI, so I can't be sure.

[proux01]

It makes master work before and after the "stdlib split", on Coq 8.20 and Rocq 9.0.

To be precise, this was already the case, the novelty being that it now works on 9.0 without Stdlib.

[proux01]

squashed

[proux01]

And BTW thanks @gares for fixing my primitive int failure (quite ashamed that I got caught by this stupid shadowing error).

[gares]

You were quite unlucky as well ;-)