Comments (13)
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.
from bedrock2.
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).
from bedrock2.
Oh, also, I think you'll need to support building without being able to download things to ../
(for the bench / opam)
from bedrock2.
Is there any reason why coq benchmarks use opam even though CI is fine with non-opam code?
from bedrock2.
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?
from bedrock2.
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
.
from bedrock2.
@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?
from bedrock2.
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
from bedrock2.
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.
from bedrock2.
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.
from bedrock2.
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.
from bedrock2.
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:
- 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.
- Support EXPECTED_COQC_VERSION=any so coq devs can bump their version numbers without breaking their CI
TODO
- Write a script that downloads and compiles or dependencies (or offload this to git submodules and makefile).
DONE
- Set up travis on our own
TODO
- Tell coq devs that bedrock2 is good to go for CI
TODO
from bedrock2.
We did this.
from bedrock2.
Related Issues (20)
- Best practice for proving loop termination in firmware? HOT 22
- Missing operators HOT 1
- Makefile doesn't work with EXTERNAL_DEPENDENCIES=1 HOT 4
- Hint Mode + again HOT 9
- bedrock1 CPS semantics vs bedrock2 postcondition semantics HOT 1
- Test suite for ToCString HOT 1
- Move MMIO.v HOT 3
- stackloop: `main` should return `int`, not `void` HOT 1
- Using multiple return values HOT 2
- Why does bedrock2 use `Load`? HOT 2
- Please create a tag for Coq 8.16 in Coq Platform 2022.09 HOT 6
- bedrock2 fails with a syntax error on Windows HOT 9
- bedrock2 lightbulb example is incompatible with native_compute HOT 5
- Less Memory-Hungry, More Principled Solution for Decidable Side-Conditions HOT 2
- Failing in coq CI HOT 1
- `make` should not run `coq` and `cc` when there's nothing to be done
- Update tested is failing with rate limits HOT 2
- Bedrock2 is broken on Coq's CI HOT 1
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 2
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from bedrock2.