Skip to content
Snippets Groups Projects
Commit a1a5cb3a authored by Janno's avatar Janno
Browse files

Add more detailed opam instructions in README.

parent 61064dbf
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 21 additions and 7 deletions
README.md
+ 21
− 7
View file @ a1a5cb3a
...@@ -12,14 +12,20 @@ The master branch is known to compile with: ...@@ -12,14 +12,20 @@ The master branch is known to compile with:
## Build ## Build
The easiest way to build the development is to use OPAM. The recommended way to build the development is using OPAM. To avoid conflicts
Go to [coq/ra](coq/ra) and then `make build-dep`. with existing packages, we recommend to create a new opam switch:
All the dependencies will be built and installed by OPAM before
the actual compilation of the development.
Manually, one can build and install Iris `opam switch ra-gps --alias-of=4.02.3`
(currently [Iris@01d12014][iris]),
and then `make` in [coq/ra](coq/ra). It should work for any compiler version upwards of 4.01.0. After compiling
OCaml, the new switch needs to be activated in your current shell. opam will
print the necessary instructions.
To find all the dependencies of ra-gps, opam needs to know about the Coq opam archive. This can be achieved by executing
`opam repo add coq-released https://coq.inria.fr/opam/released`
Now, go to [coq/ra](coq/ra) and execute `make build-dep` to install all
dependencies of ra-gps. Finally, execute "make" to build the development.
## Structure ## Structure
...@@ -28,6 +34,7 @@ The Coq development is in folder [coq/ra/](coq/ra). ...@@ -28,6 +34,7 @@ The Coq development is in folder [coq/ra/](coq/ra).
* The operational semantics is in [machine.v](coq/ra/machine.v). The language is in [lang.v](coq/ra/lang.v). * The operational semantics is in [machine.v](coq/ra/machine.v). The language is in [lang.v](coq/ra/lang.v).
* The base logic is in the [base/](coq/ra/base) folder. * The base logic is in the [base/](coq/ra/base) folder.
Each base rule is proven in a separate file. Each base rule is proven in a separate file.
<<<<<<< Updated upstream
* iRSL's main rules are in [rsl_instances.v](coq/ra/rsl_instances.v). The model is in [rsl.v](coq/ra/rsl.v). * iRSL's main rules are in [rsl_instances.v](coq/ra/rsl_instances.v). The model is in [rsl.v](coq/ra/rsl.v).
* Non-atomic rules are in [na.v](coq/ra/na.v). * Non-atomic rules are in [na.v](coq/ra/na.v).
* iGPS's rules are in the [gps/](coq/ra/gps) folder. The model is in [gps/shared.v](coq/ra/gps/shared.v) * iGPS's rules are in the [gps/](coq/ra/gps) folder. The model is in [gps/shared.v](coq/ra/gps/shared.v)
...@@ -55,3 +62,10 @@ The Coq development is in folder [coq/ra/](coq/ra). ...@@ -55,3 +62,10 @@ The Coq development is in folder [coq/ra/](coq/ra).
[iris]: https://gitlab.mpi-sws.org/FP/iris-coq/commit/01d12014855abe6adaea20bbb35b1e9beadff14e [iris]: https://gitlab.mpi-sws.org/FP/iris-coq/commit/01d12014855abe6adaea20bbb35b1e9beadff14e
=======
* iRSL's main rules are in `rsl_instances.v`. The model is in `rsl.v`.
* Non-atomic rules are in `na.v`.
* iGPS's rules are in the `gps` folder. The model is in `gps/shared.v`
* Examples are in the `examples` folder.
* `tests/message_passing.v` contains a closed proof of MP without Iris statements.
>>>>>>> Stashed changes
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment