continuous integration

[andres-erbsen]

Spinned off from coq/coq#7878

It would be great if bedrock2 could be built as a part of the Coq continutous integration system so that coq changes do not break it. Secondarily, it would also be nice to have a computer nanny us to make sure we don't break the build ourselves. I think there are three blockers for this:

1. Continually ensure that bedrock2 builds with the latest coq release and with coq master.
2. Support EXPECTED_COQC_VERSION=any so coq devs can bump their version numbers without breaking their CI
3. Write a script that downloads and compiles or dependencies (or offload this to git submodules and makefile).
4. Set up travis on our own
5. Tell coq devs that bedrock2 is good to go for CI

@samuelgruetter is this a direction where you would like to see bedrock2 go? If so, would you like to do some of the above steps yourself, or give me guidance on how to do them in a way that does not conflict with your plans?

[JasonGross]

Note that, additionally, if you want this to be tested on the Coq bench, there also needs to be an opam package. I can take care of this (as well as ~ step 5 above of making a PR that adds bedrock2 to the Coq CI), once 1-4 are completed, if you let me know which dependencies are expected to be installed via opam (or similar) (rather than locally available via submodules), and what the version constraints on those dependencies are (which I'm guessing will just be "= dev" or whatever it is to say that it's the one for the dev version of Coq).

[JasonGross]

Oh, also, I think you'll need to support building without being able to download things to ../ (for the bench / opam)

[andres-erbsen]

Is there any reason why coq benchmarks use opam even though CI is fine with non-opam code?

[samuelgruetter]

I'm certainly pro CI!
Your steps 1-5 look good to me, but I'd wait doing them until we have clarified the role of opam.

Regarding 3) I wouldn't like to use git submodules because diamond dependencies will bite us.

Some days ago I actually tried to use recursive make to build bbv and riscv-coq, but gave up after a few hours because I couldn't tell makefile that coqdep-generated dependencies going pointing outside of bedrock2 have to be built using recursive make (various things which you'd expect to work didn't work...)

My workflow involves often modifying bbv, riscv-coq, bedrock2, and the current setup allows me to do that quite productively. What would that look like using opam? In particular, could I test the effects of changes in one repo in another repo without committing and updating version numbers?

[JasonGross]

CI runs on travis, but the bench runs on an INRIA machine which times/profiles opam install. I think the easiest thing to do is to either use submodules or just have them be, e.g., ./bbv rather than ../bbv.

[samuelgruetter]

@JasonGross how much would you worry about diamond dependencies like this one: Suppose in a few months kami switches to using bbv rather than an integrated copy of it, and they prove some kami processor correct agains riscv-coq, and I want to create a repo called end-to-end which depends both on the kami processor and bedrock2, so it will depend on two different types of bbvs: The kami submodule, and the riscv-coq submodule. So I guess I'd have to write some kami-bbv<->riscv-bbv word conversion boilerplate. How bad do you think this will be? So far I classified it as very bad and therefore excluded submodules and ./bbv folders from my consideration, but I start wondering which of these two is less bad... Any advice?

[vmurali]

I don't have an opinion about bedrock's CI.

But, I am actively using the bbv repo (not the plv/kami version) in sifive/kami and I am not using git submodules to avoid all the problems it brings with it. I don't see why submodules would solve any of your problems @samuelgruetter

[JasonGross]

I'd say then you should make both repos support a global/COQPATH-based installation of bbv, and both repos should be compatible with either the tip of bbv, or a particular tag.

[andres-erbsen]

I think the only sustainable solution to diamond dependency situations with shared interfaces like the one you describe is to have all code in the same repo, perhaps using git-merge-subtree to integrate with separate development repositories. this would also solve the CI compatibility issues, allowing git clone of that repo to build without permissions to the parent directory. I think we could emulate that by hacking together an umbrella repo that has git submodules for all repos which you want to use the sibling trajectory setup for.

[samuelgruetter]

I like the "umbrella repo" idea! Here's how I understood it:

Each "participating repo" should satisfy the following requirement:

It has to be possible to configure the repo such that it builds with all shared dependencies as siblings.

bbv, riscv-coq and bedrock2 satisfy this already, and if I understand correctly, sifive/Kami as well, and repos supporting a COQPATH-based installation of bbv would satisfy this requirement as well.

Whether or not an individual repo wants to use git submodules would be up to their owners, as long as they satisfy the above requirement.

Given this, the "umbrella repo", called eg bedrock2-ci, would consist of (currently) 3 git submodules (bbv, riscv-coq, bedrock2), and a makefile which invokes recursive make on these three submodules.
bedrock2-ci would get CI, a travis file and opam packaging.

[samuelgruetter]

I made an umbrella repo here: https://github.com/mit-plv/bedrock2-ci
It builds locally on my machine with Coq 8.7.2.

Going through @andres-erbsen's original list of blockers:

1. Continually ensure that bedrock2 builds with the latest coq release and with coq master.

I haven't tried yet with other Coq versions than 8.7.2.

2. Support EXPECTED_COQC_VERSION=any so coq devs can bump their version numbers without breaking their CI

TODO

3. Write a script that downloads and compiles or dependencies (or offload this to git submodules and makefile).

DONE

4. Set up travis on our own

TODO

5. Tell coq devs that bedrock2 is good to go for CI

TODO

[samuelgruetter]

So I added a DEPS_DIR option to bedrock2's Makefile to configure where the dependencies (bbv and riscv-coq) are, so we can now use the following two setups at the same time:

• They can be siblings of bedrock2.
  • CI: bedrock2-ci has a Travis build which ensures that this setup works.
  • Advantage: Avoids diamond problems when combining with other repos which also use bbv and/or riscv-coq.
• They can be git submodules in bedrock2/bedrock2/deps.
  • CI: bedrock2 now has its own Travis build too.
  • Advantage: I think I will use this setup from now on, because it allows me to make changes to bedrock2 and record what versions of bbv and riscv-coq it depends on in just one commit, instead of having to make an additional commit in bedrock2-ci.
  • Advantage: If Coq developers want to PR a patch against bedrock2, they only need to make one PR instead of two.

I also removed the EXPECTED_COQ_VERSION check.

[andres-erbsen]

We did this.