- Nov 30, 2016
-
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Ralf Jung authored
-
-
Ralf Jung authored
We now include the git commit in the version number seen by opam. As a consequence, opam can handle the reinstallation tracking for us, so everything gets much simpler.
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
- Nov 29, 2016
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Also, perform some refactoring.
-
Jacques-Henri Jourdan authored
-
- Nov 28, 2016
-
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Ralf Jung authored
-
Ralf Jung authored
New opam-based CI and build system Submodules are gone. If you have opam set up, `make build-dep` will install the right version of everything. This is *not* exactly what we discussed last week; I think I found something better. In particular, this approach lets us also figure out for historic lambdaRust versions, which commit of iris they needed. No magic branches in other repositories are needed, everything is local here. Essentially, since the `opam` files do not support documenting detailed enough version information, I added a new file `opam.pins` that "enhances" the opam file appropriately. This file contains pins (one per line) that have to be set to compile lambdaRust. The script in `build/opam-pins.sh` applies those pins - and crucially, it does so recursively: When it finds a pin that is one of our git repositories, it will download the `opam.pins` files for *that* commit and also apply its pins. So if lambdaRust pins a particular commit of iris, and iris pins a particular commit of the prelude, then doing `make build-dep` in lambdaRust will follow this transitive chain and install the correct versions of iris and the prelude. Cc @jjourdan @robbertkrebbers See merge request !2
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Robbert Krebbers authored
In particular, I started changing some lemmas in borrow.v to not unfold everything right away. Unfolding everything right away yields very big goals that do not fit in one screen and makes stuff slow.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
- Nov 27, 2016
-
-
Jacques-Henri Jourdan authored
-
- Nov 26, 2016
-
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
- Nov 25, 2016
-
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-