Rocq 9.0.0

[shilangyu]

TODO:

• alectryon does not work, SerAPI does not support Rocq 9.0.0: Alectryon for Rocq 9.0 cpitclaudel/alectryon#104
• There are some warnings regarding Focus.v Notation having conflicts
• Double check extraction works correctly
• Double check if the nix flake needs updates

When the new dune plugin is released, we can use ocaml/dune#11752

[Ef55]

Glad to see Warblre updated to Rocq!

FYI the pull request you pointed to was merged a few hours ago (may still take some time before a new version of dune gets released though).

I attempted to update the flake to Rocq 9.1, but it would seem I've somehow run into rocq-prover/rocq#20128 :

Details

dune build
File "engines/ocaml/dune", lines 10-13, characters 0-102:
10 | (coq.extraction
11 |  (prelude Extraction)
12 |  (extracted_modules Extracted)
13 |  (theories Warblre Ltac2 Stdlib))
*** Error: Anomaly
           "Uncaught exception Fl_package_base.No_such_package("rocq-runtime", "")."
           Please report at http://rocq-prover.org/bugs/.
File "mechanization/dune", lines 3-6, characters 0-72:
3 | (coq.theory
4 |  (name Warblre)
5 |  (package warblre)
6 |  (theories Ltac2 Stdlib))
*** Error: Anomaly
           "Uncaught exception Fl_package_base.No_such_package("rocq-runtime", "")."
           Please report at http://rocq-prover.org/bugs/.
File "engines/js/dune", lines 10-13, characters 0-102:
10 | (coq.extraction
11 |  (prelude Extraction)
12 |  (extracted_modules Extracted)
13 |  (theories Warblre Ltac2 Stdlib))
*** Error: Anomaly
           "Uncaught exception Fl_package_base.No_such_package("rocq-runtime", "")."
           Please report at http://rocq-prover.org/bugs/.

It seems to just be the latest nix issue related to the Rocq renaming. I don't think there is anything we can do on our side, so I'd be tempted to tell you to disregard this issue, as long as everything else is working.

[shilangyu]

Thanks for the flake update Noé :)

It seems to just be the latest nix issue related to the Rocq renaming. I don't think there is anything we can do on our side, so I'd be tempted to tell you to disregard this issue, as long as everything else is working.

We have to wait for alectryon, maybe by that time nix will get fixed

FYI the ocaml/dune#12035 you pointed to was merged a few hours ago (may still take some time before a new version of dune gets released though).

I think yes, it might take a while. I will keep a close eye.

[shilangyu]

The new dune might be released soon: ocaml/dune#12788 (comment)

I pushed a WIP commit (won't compile unless you upgrade dune with opam pin add dune.3.21.0 https://github.com/ocaml/dune.git#6e9d965bb5bbadfe9cbf89314cb6f8ecaa845bd9). It migrates to the new dune plugin. I also removed all _CoqProject files. I am not sure they are useful at all since we are using dune anyway? If it is useful, we can consider instead using the dune's (generate_project_file) option which would generate it automatically.

[Aurele-Barriere]

Thanks a lot! The _CoqProject file is actually useful for some editors, I think proof-general uses it for instance.
I didn't know about dune's generate_project_file, that could be a better way yes!

[shilangyu]

Thanks a lot! The _CoqProject file is actually useful for some editors, I think proof-general uses it for instance. I didn't know about dune's generate_project_file, that could be a better way yes!

I can enable it, but just for clarity: I don't think it produces commitable files. They contain absolute paths (I wonder if it is even expected). So users will have to run dune build first (which, I think is a fair requirement)

[Aurele-Barriere]

Running dune build first seems fair to me too

[Ef55]

Some updates:

• I updated the nix stuff to use the "bleeding-edge" versions of rocq/dune. Seems like everything builds successfully on my end now! I'll have to tweak the nix files again once these bleeding-edge versions become available in nixpkgs (we don't need to wait for that to merge though).

• I fixed many (if not all) of the new warnings.

• I double checked that _RocqProject was needed; generate_project_file works great though.

• I'm getting this big message in my terminal when running dune build, which I don't remember happening in the past (I may be misremembering though):

  Details

       = Success                            
           (NonGlobalResult
              (Exotic
                 (exec_array_exotic 2 [104; 101; 108; 108; 111] [
                    Some [108]] None None None)))
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.039 secs (0.037u,0.001s) (successful)
       = Success (NonGlobalResult Null)
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.003 secs (0.003u,0.s) (successful)
       = Success
           (NonGlobalResult
              (Exotic
                 (exec_array_exotic 2 [104; 101; 108; 108; 111]
                    [Some [108; 108]] None None None)))
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.03 secs (0.03u,0.s) (successful)
       = Success
           (NonGlobalResult
              (Exotic
                 (exec_array_exotic 0 [97; 98] [Some [97; 98]] None None None)))
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.051 secs (0.051u,0.s) (successful)
       = Success
           (NonGlobalResult
              (Exotic
                 (exec_array_exotic 0 [97; 98] [Some [97; 98]; Some [98]]
                    (Some []) None None)))
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.074 secs (0.071u,0.002s) (successful)
  

• I (finally) reported the melange warning: Using new.target in raw JS results in a warning melange-re/melange#1685

• For some reason I have yet to understand, our extraction hacks to map Rocq's bigints to Ocaml/Js bigints stopped working properly (run dune test to see failing tests). I'll take another look later this week.

• Change SpecMerger remote&commit in flake once Bump versions in nix flake SpecMerger#2 is merged

[shilangyu]

Thank you!

1. Regarding the message, it seems to have been present before this PR already (see the dune build step): https://github.com/epfl-systemf/Warblre/actions/runs/18123838898/job/51574355291?pr=5
2. We merged your SpecMerger PR

[Ef55]

1. Great, one less thing to fix!
2. I'll update the flake, thx

[Ef55]

OK, I figured out where the extraction issue came from: it was caused by the split of the Pos library into two pieces (one in the Corelib, the other in the Stdlib), which caused some weirdness in the extraction.

Everything seems good on my side. I guess the last thing to fix is the CI (and re-enabling alectryon when it gets updated). @shilangyu will you take care of the CI, or should I take a look? The current failure seems related to the install of dune, which means you might be better geared to investigate than I am (since the CI does not use nix).

[shilangyu]

Thanks for the extraction fix! I think now we just wait for alectryon. The CI is failing because we now use the unreleased dune version (which just got an alpha release). Once it is released, the CI will work again.

[shilangyu]

Dune 3.21 was tagged so I assume it will be soon released on opam. So only alectryon is left. What are your thoughts on merging this with a broken alectryon setup (and adjusting the CI/docs/etc to reflect this)?

[Ef55]

Alectryon is used to generate a webpage for an exemple, but that webpage is never pushed anywhere.
As far as I'm concerned, we can just disable that to (temporarily?) drop the Alectryon dependency.

[shilangyu]

I have disabled alectryon for now and opened an issue about it #7.

I am marking this PR ready for review. If you approve those changes please feel free to merge.

[Ef55]

Just one nitpick: are we officially supporting 9.0, or only 9.1 onward only?
The dune files requires Rocq >=9.0, but I only tested 9.1, and the CI uses 9.1 as well.

Otherwise everything looks good to me!

PS: Apologies for the delay in my response ^^'

[shilangyu]

EDIT: eh, the rocq-prover meta package does not have 9.1. Let's just add 9.0 to the CI.

There is not much difference between 9.0 and 9.1, so instead of supporting both I suggest we just explicitly support 9.1 onwards. I will push a fix

[Aurele-Barriere]

Thank you so much to the both of you,
We'll wait just a bit more for a possible upgrade of Alectryon, but everything looks good to me

[cpitclaudel]

0001-examples-Replace-Restart-with-separate-lemmas.patch

I seem to have lost permissions on this repo in the move to the Linden org, so here's a patch. I think a patch like this one would be needed to step through examples.v in vsrocq independently of Alectryon.

I've fixed the Alectryon issue reported by @shilangyu (thanks!), but I'm not sure why we run Alectryon on this repo. Wouldn't the simplest be to remove it, especially given that the file that we give it (Example.v) is a coqdoc file?

(Also doesn't Example.v need a _RocqProject?)

[shilangyu]

This PR is ready for merging. I will leave the decision of removing/keeping Alectryon up to you @Ef55 @Aurele-Barriere.

@Ef55 The flake will need updating for the update/removal of Alectryon probably.

[Aurele-Barriere]

I'd be on board with removing Alectryon from this repo

[cpitclaudel]

Don't we need to generate_project_files also for the example? Otherwise the warblre import doesn't work for me in VSCode.

[shilangyu]

Don't we need to generate_project_files also for the example? Otherwise the warblre import doesn't work for me in VSCode.

I will include it in the next commit depending on whether we keep or remove Alectryon. In fact, I will optimistically remove Alectryon now and if Noé would prefer to keep it, I will revert the commit.