move from coq to rocq

[damien-pous]

Hi @palmskog

I'm trying to prepare a 9.0.0 version ; here is a pr for using rocq only, not the transitional packages.
Everything compiles with [make] with just rocq-prover 9.0.0

There are still things I don't know how to do (Makefiles for documentaion, meta files, compilation with dune), though.

Please tell me if I should do things differently.

[palmskog]

@damien-pous is this specifically for 9.0 or is it Rocq master compatible? Maybe best would be to do Rocq master version first, then merge into v9.0 and adapt.

[damien-pous]

Hi Karl,
I was targeting Rocq 9.0.0 for rocq-platform.
I'll check now if it works with Rocq master later this morning.

[palmskog]

But then it would make sense for this PR to target v9.0 branch, right? Unfortunately, may take merging...

[damien-pous]

It does compile with rocq dev too (with two new warnings which would be easy to fix)
Ideally, we would apply it to master, and merge or restart v9.0 from there? (I think v9.0 was never published)

[damien-pous]

I have a merge here:
https://github.com/damien-pous/aac-tactics/tree/v9.0

which also compiles (using make) under both Rocq master and 9.0.0

[damien-pous]

Hi again @palmskog ,

I've tried again to fix dune compilation (with coq-core compatibility shim, I had not understood they would be necessary before)

But I stumble upon the following problem: it seems the stdlib path is not correctly bound to Stdlib, so that I cannot import its modules, unless I explicitly add an "-R path Stdlib" to the dune flags.