[mach] Update

[franziskuskiefer]

Tracking the update sub-command

• set upstream repository or directory #76
• copy all needed files (msvc, c89)
• Streamline ./mach update #12
• write out revision of all dependencies
• make snapshot of all dependencies in a docker image
• only copy what's really needed (using dependency analysis)

[protz]

Just now looking at this... can we discuss design a little bit for the last item? I'm trying to understand what you have in mind... here's my best guess:

• Somehow mach will write out somewhere the git revisions + branches of all our dependencies (basically the Everest script design, with an equivalent of hashes.sh)
• What you want is a Dockerfile (also, probably, based on the Everest ones) that can build F*/KReMLin/HACL* for a given set of revisions (probably passed from the mach script as Dockerfile variables).
• mach docker launches docker build with suitable values for the revisions and the user ends up with a docker container that contains a working environment and then maybe mach opens up a bash instance with the docker container

Is that close to what you had in mind? Would this be for debugging purposes, for verification work and to make things easier...?

Thanks!

[franziskuskiefer]

Let's first define how the setup looks like and what it is that we need.

• There's the HACL* F* repository with all the specs, proofs etc. that is used to generate the C code
• There are dependencies of HACL* F* such as KReMLin and F*
• There are pieces of code such as Vale that we consider external input. In future this might also be other primitives in Jasmin etc.

We need

• to be able to update the HACL* C library when there are upstream changes in HACL* F*
  • maybe we also need to able to update KReMLin or F* independently, but I'd suggest to force a HACL* F* update in that case
• to be able to specify new external dependencies or version that are then pulled in when prompted
• to be able to maintain old HACL* C releases

The docker image is primarily for the last point.
I think in most cases it's fine to say that we only fix high-severity issues in old releases and do so manually in the C code. For all other cases we require the consumer to update to a new version. Nonetheless, we should be able to reproduce the state of each release to work on them (reproduce errors, do verification work, etc).
In order to do that we need a snapshot of all the dependencies as long as they don't have releases (which would be the ideal case that we might reach at some point).

On a high-level the workflow should probably something like mach release ... creates a git tag and docker image with a snapshot of all dependencies of HACL* C in this tag to later jump in and use. A mach release --publish or something might also push the tag and docker image to a remote. And to use the docker image later we'd need something like mach docker --run --version=x.xx.x that spawns (potentially first pulls) a docker instance with the specified versions and gives the user a shell in there to work on that release.
For testing and development purposes we probably also want a mach docker --tag --version=x.xx.x or something similar to just create a new docker image for the current state. We'll have to iterate on what the exact commands are that we need when using them.

It would probably also be good (as you say) to store the docker/release config (git revisions) additionally in a file in the repo for reference and to be able to reproduce lost docker images.

Does this make sense?
I think it's pretty much the same to what you wrote.