Experiment: dunify proofs

[eponier]

This is an experiment to port the Coq part of Jasmin to dune. Instead of just one dune file (which is another valid option), I tried to use one dune file per directory, to split the sources into components, with clear dependencies between one another. This PR is more for starting discussions about whether we want to go in that direction.

Pros of porting to dune:

• benefit from caching of the build
• getting closer to have only dune as the build system

Cons of porting to dune:

• we have to list the transitive dependencies in the theories stanza in the dune file, but actually only sometimes, I don't understand the logics
• the coq.extraction stanza must explicitly list the OCaml files created by extraction, including all the files coming from the Coq stdlib, this is ugly
• the _CoqProject files may still be needed for easy interactions with editors (there is a PR in which dune generates them automatically, or we have to use dune coq top somehow), meaning that we duplicate information between dune files and _CoqProject files

Pros of having one dune file per directory:

• clearer dependencies between components, with a check at compilation that we don't introduce wrong dependencies between the components

Cons of having one dune file per directory:

• files in other directories are considered coming from another library, so we have to use From other_directory Require Import ... to do the imports.
• in the current implementation, the pp_error type is not known in arch so cannot be used there, while there were a few occurrences in arch_extra.v. I tried to put just a string there, it works rather okay, but I don't know if this was the best option.

Current limitations:

• we may go further in the splitting. For instance, compiler depends on arch, while only the lowest part of compiler depends on it. So we could split compiler into an arch-dependent and an arch-independent parts.
• maybe the most interesting separation to check is that the compiler does not depend on the proofs, and this is not done at all here
• one thing that I'd like also at some point would be to have a compiler target that really builds the compiler and not the other tools (CT, SCT, evaluator, safety checker...), including on the Coq side. There are a few Coq files that are needed for the evaluator but not for the compiler. But since extraction from Coq to OCaml is monolithic, I fail to see how to do the split easily.

[vbgl]

Thanks for exploring this. I really don’t like the following: “we have to use From other_directory Require Import … to do the imports.” I already have a hard time finding source files in the various directories, I fear that this will just exacerbate the problem.

[eponier]

Thanks for exploring this. I really don’t like the following: “we have to use From other_directory Require Import … to do the imports.” I already have a hard time finding source files in the various directories, I fear that this will just exacerbate the problem.

Two technical solutions to this:

• use only one dune file, and we can keep Require Import ... without From
• calling the dune targets jasmin.xxx instead of xxx and we can use From jasmin Require Import ... whatever the xxx is

Taking a step back, I think not knowing where files are located reveal that the file hierarchy is not perfect at the moment. So the best solution might be to agree on some changes to it. For me, apart from asm_gen.v and asm_gen_proof.v that should really be in compiler, and seq_extra.v and the like that I can't remember whether they are in 3rdparty or ssrmisc, I think the situation is not that bad. But we could also change the organization completely, personally I don't mind, the important thing is just that it makes sense. Other compilers have frontend and backend directories for instance.

To some extent, I think having a more rigid build system might help for that, because it will be too painful to have something that does not make sense.