Emilio Jesús Gallego Arias

[coqdep] Make strict mode the default.

7

Strict mode means we fail when we cannot locate a file. This is an experiment before implementing `-modules`.

[draft] Preliminary support for building with Dune

4

Dear CompCert developers, this is a proof-of-concept highlighting a full build of x86 using the Dune build system. The PR is not meant to be merged yet, but as a...

[jscoq] Migration to Flèche as document checking bakend.

1

We replace the STM backend with Flèche, a continous, full-hybrid-document checker. The new API is much simpler (and modelled after LSP): jsCoq just sends the full document, and Flèche will...

[ci] Make pull request generate node artifacts that can be installed by users / developer on the npm side

2

Discussing with Bernard Boey Khai Chen , it came to our attention that it would be great if our CI could generate artifacts that are directly usable from node, automatically....

A critical need some jsCoq users have is to persist a session where for example students do solve exercises and make progress. Closely related to this seems the need for...

After the jscoq and wacoq frontend were merged, we should unify the ML backend. As far as I can see, there is nothing that should impede this [likely wacoq may...

[addons] Meta Coq

1

Would be great to add metacoq to the official 8.10 build, cc @TheoWinterhalter

After #100 , jsCoq now depend on SerAPI, and SerAPI also depends on some jsCoq libraries :) However the current setup has a few nits to clean up, for example,...

Integration of udoc, generation of jscoq-aware html?

4

We currently provide https://github.com/ejgallego/udoc as a way to go from `.v` files to `html` ones with jscoq support. However the output is a bit rough; what is the future of...