fix and update alectryon #2340
fix and update alectryon #2340
Conversation
Alizter
force-pushed
the
push-mypspyvxqnuy
branch
2 times, most recently
from
83d5a72 to
7c2a105
Compare
Signed-off-by: Ali Caglayan <[email protected]>
Alizter
force-pushed
the
push-mypspyvxqnuy
branch
from
7c2a105 to
16f7bec
Compare
|
Looks like there is still a build issue. BTW, do you know if alectryon is using more than one core when building? It would be great to speed it up if possible. |
|
It's just a python script that essentially goes through all the proofs all at once. There is surely a way to do this work concurrently, but I will leave that to a future PR. We also seem to be failing to reuse the previous build. |
The previous one had all sorts of weird opam pins inherited from the docker image and was generally difficult to work with. I previously updated the nix flake to be able to run the alectryon script, so we just use the develoment environment there to run it in CI. We can still improve the actual build of the alectryon docs further by introducing concurrency, but at least this should fix the issues with CI. Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
|
Alectryon was starting coq-lsp and querying it for every goal one at a time. That is slow. I've instead used coq-lsp's Coq compiler |
|
Wow, that sounds great! It's much faster than before. Does it also use multiple cores? |
Yes, since we are generating a bunch of rules, dune is able to run them concurrently. |
|
We will need to make sure that the wiki links are correctly working when the elctryon website is deployed. Having a look locally at |
|
Ok, looks good to me! |
|
I'll do another pass on this in the evening before merging. |
|
I did a self-review. There are some issues:
I think we should hold off merging for now until I can address this points. |
|
Green CI is also misleading, the HTML might be broken in places I haven't checked. |
2 participants
I broke this job in an earlier PR on purpose. We fix the CI job for it here and change the backend that alectryon was using. It used to use serapi, but that has now been subsumed by rocq-lsp. We update the submodule alectryon to a version that understands it.