Emilio Jesús Gallego Arias

[dune] [test-suite] Port the test suite to Dune

35

This is an in-progress PR to port the test suite to Dune. Main design principles are: - use the standard `runtest` infrastructure, and declare all the dependencies correctly so the...

[dune] [build] Enable native compilation for the standard library.

16

(Mostly) fixes #8860 ; see documentation for more information. There are some open issues with regards to our CI + dune, so far we build everything in dev mode, except...

[coqdep] Don't "canonize" files.

5

"Canonization" is a fragile (and expensive) process, instead, we require that files passed to coqdep match the layout given in the `-R` / `-Q` options.

[build] Add support for code coverage

88

Closes #10267 This PR went into a few iterations due to build system changes; it is in final form now. A couple of notes: - the instrumentation support we use...

[coqdep] Further cleanup of the loadpath API

5

In particular we remove the `coqlib` field which was just used to suppress a warning. This brings `coqdep/loadpath` closer to `vernac/loadpath.ml`, but still a way to go. Many differences are...

[build] [vm] Fix flags declaration in dune file.

14

Before Dune 2.7, Dune was implicitly adding the `:standard` set of variables to our CC invocation for `kernel/byterun`. This set is `-O2 -fno-strict-aliasing -fwrapv -fPIC`, but after discussion we want...

[libobject] Store definition location in the .vo files

30

This has been a long-requested feature that we need to implement it properly for users; after a bit of discussion with Ali we decided to go ahead. For now, the...