Initial commit

.github/workflows/docker-image.yml

@@ -0,0 +1,19 @@
+name: Docker CI
+
+on:
+  push:
+    branches: [ "main" ]
+  pull_request:
+    branches: [ "main" ]
+  workflow_dispatch:
+  schedule:
+  - cron: 0 0 1 * * # once a month
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Check out repos
+      uses: actions/checkout@v3
+    - name: Build the Docker image
+      run: docker build . --file Dockerfile --tag axsl:$(date +%s)

.gitignore

@@ -0,0 +1,13 @@
+_build/
+_opam/
+.vscode/
+
+.*.aux
+*.vo
+*.vok
+*.glob
+*.v.b
+
+.lia.cache
+
+.DS_Store

Dockerfile

@@ -0,0 +1,29 @@
+ARG BASE_TAG="latest"
+FROM coqorg/coq:8.16.1-ocaml-4.14.1-flambda
+
+COPY --chown=coq . /artifact/axsl
+WORKDIR /artifact
+
+# hadolint ignore=SC2046
+RUN sudo apt-get update && sudo apt-get install zlib1g-dev -y
+
+RUN eval $(opam env --set-switch) \
+    && opam update -y -u \
+    && opam config list && opam repo list && opam list \
+    && opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+
+RUN git clone https://github.com/rems-project/coq-sail \
+    && cd coq-sail \
+    && git checkout aeca2c5 \
+    && opam pin . -y
+
+RUN opam install axsl/. --deps-only -y
+
+RUN git clone https://github.com/tchajed/iris-named-props.git \
+    && cd iris-named-props \
+    && git checkout 327119f \
+    && opam pin . -y
+
+RUN opam list \
+    && cd axsl \
+    && dune build --display short

INSTALL.md

@@ -0,0 +1,106 @@
+# Building from scratch
+
+## Compiling the development with Docker
+
+We recommend compiling the development using Docker. To do this,
+
+1. Make sure you have [Docker](https://docs.docker.com/get-docker/) installed.
+2. Run `docker build -t="axsl:popl" .` in the source code directory (which contains a `Dockerfile`) 
+to build the Docker image.
+
+The building process may take up to one hour, including installing dependencies and compilation. 
+
+Optionally, you can follow this by executing `docker run -i -t axsl:popl` to start a container with
+the freshly built image and access an interactive shell inside it.
+
+### Troubleshooting
+
+In order to build the development, you might have to increase the amount of
+memory allocated to a running Docker container. For instructions, see
+[here](https://stackoverflow.com/questions/44533319/how-to-assign-more-memory-to-docker-container).
+
+## Manually Installing with opam
+
+### Opam and ocaml
+
+All dependencies install instruction assume you can use `opam`. If needed,
+instructions are available here: https://opam.ocaml.org/doc/Install.html.
+
+You need to add the coq opam repository for some of the dependencies:
+```
+opam repo add coq-released https://coq.inria.fr/opam/released
+```
+
+
+### Dune
+
+This project uses the dune build system. It can be installed with:
+```
+opam install dune
+```
+
+
+### Coq
+
+Install Coq `8.16.1`
+```
+opam pin coq 8.16.1
+```
+
+### Coq libraries
+
+#### Iris and stdpp
+
+You need to add the iris opam repository to install Iris and stdpp :
+```
+opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+```
+
+This development uses a development version of Iris and stdpp:
+```
+opam install coq-iris.dev.2023-08-11.1.81f394da -y
+```
+
+This development uses an unstable extension of `stdpp`: 
+```
+opam install coq-stdpp-unstable.dev.2023-08-03.3.4be5fd62 -y
+```
+
+#### iris-named-props
+
+This development uses a small Iris extension `iris-named-prop`.
+
+Clone it with
+```
+git clone https://github.com/tchajed/iris-named-props.git
+```
+
+In the cloned directory, check out to the version that has been tested:
+```
+git checkout 327119f
+```
+
+Install with opam:
+```
+opam pin . -y
+```
+
+
+#### Coq Record Update
+
+This repository use the Coq record update library. To install it do:
+```
+opam install coq-record-update
+```
+
+#### Dependencies of system-semantics
+
+Install the libraries listed in `system-semantics/INSTALL.md` but not mentioned above
+
+### Build the development
+
+In the directory, run:
+
+```
+dune build
+```

coq-iris-axiomatic-arm.opam

@@ -0,0 +1,36 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+maintainer: ["Zongyuan Liu <[email protected]>"]
+authors: [
+  "Zongyuan Liu <[email protected]>"
+  "Angus Hammond <[email protected]>"
+  "Jean Pichon-Pharabod <[email protected]>"
+  "Thibaut Pérami <[email protected]>"
+]
+homepage: "https://github.com/logsem/AxSL"
+bug-reports: "https://github.com/logsem/AxSL/issues"
+depends: [
+  "dune" {>= "3.9"}
+  "coq" {= "8.16.1"}
+  "coq-record-update" {= "0.3.2"}
+  "coq-hammer-tactics" {= "1.3.2+8.16"}
+  "coq-stdpp" {= "dev.2023-08-03.3.4be5fd62"}
+  "coq-stdpp-unstable" {= "dev.2023-08-03.3.4be5fd62"}
+  "coq-iris" {= "dev.2023-08-11.1.81f394da"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/logsem/AxSL.git"

dune-project

@@ -0,0 +1,30 @@
+(lang dune 3.9)
+(name coq-iris-axiomatic-arm)
+(using coq 0.8)
+
+(generate_opam_files true)
+
+(authors
+ "Zongyuan Liu <[email protected]>"
+ "Angus Hammond <[email protected]>"
+ "Jean Pichon-Pharabod <[email protected]>"
+ "Thibaut Pérami <[email protected]>")
+
+(maintainers
+ "Zongyuan Liu <[email protected]>")
+
+(source
+ (github logsem/AxSL))
+
+(package
+  (name coq-iris-axiomatic-arm)
+  (allow_empty)
+  (depends
+    (coq (= 8.16.1))
+    (coq-record-update (= 0.3.2))
+    (coq-hammer-tactics (= "1.3.2+8.16"))
+    (coq-stdpp (= "dev.2023-08-03.3.4be5fd62"))
+    (coq-stdpp-unstable (= "dev.2023-08-03.3.4be5fd62"))
+    (coq-iris (= "dev.2023-08-11.1.81f394da"))
+  )
+)