VO files are, at the time of writing, made of mashaled OCaml memory. Not easy to access using external tools.
This project aims at reorganizing their format and contents in order to enable third party tools.
Documentation for Opaque says no tactic should unfold an Opaque constant. This is far from being the case today, mainly because conversion functions have a default value for transparent_state that is bypassing all user provided Opaque directives. This project is about fixing it step by step, which is a bit tricky because many external projects and the standard library rely on the bug.
The bytecode (vm_compute) and native (native_compiler) of Coq duplicate a significant amount of infrastructure, with subtle differences (in representation of values, compilation schemes, etc). Resolving the differences will make it possible to factorize a lot of code, reaching a state where there is only one compiler with two back-ends.
The overall goal is to reduce the number of distinct implementations for similar tactics and as such the number of lurking bugs.
The only way to achieve this without breaking compatibility too much is by listing the various discrepancies and making the new implementation very flexible.
Sometimes automatic tests are failing, not because there is an actual bug, but because the tests are fragile and fail randomly from time to time. The goal of this project is to list instances of non-deterministic tests and fix them.