Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Marianna Rapoport
iris-coq
Commits
d5ff27dc
Commit
d5ff27dc
authored
Mar 17, 2016
by
Ralf Jung
Browse files
more links in README
parent
3fdc8784
Changes
1
Hide whitespace changes
Inline
Side-by-side
README.md
View file @
d5ff27dc
# PREREQUISITES
# IRIS COQ DEVELOPMENT
This is the Coq development of the
[
Iris Project
](
http://plv.mpi-sws.org/iris/
)
.
## Prerequisites
This version is known to compile with:
...
...
@@ -11,7 +15,7 @@ fetch the development branch yourself). Iris compiles fine even without this
patch, but proof bullets will only be in 'strict' (enforcing) mode with the
fixed version of Ssreflect.
# B
UILDING INSTRUCTIONS
#
# B
uilding Instructions
Run the following command to build the full development:
...
...
@@ -22,7 +26,7 @@ running:
make install
# S
TRUCTURE
#
# S
tructure
*
The folder
`prelude`
contains an extended "Standard Library" by Robbert
Krebbers
<http://robbertkrebbers.nl/thesis.html>
.
...
...
@@ -36,7 +40,7 @@ running:
*
The folder
`barrier`
contains the implementation and proof of the barrier
<http://doi.acm.org/10.1145/2818638>
.
# D
OCUMENTATION
#
# D
ocumentation
A LaTeX version of the core logic definitions and some derived forms is
available in
`docs/iris.tex`
.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment