Upstream everything to base repo

.github/workflows/docker-action.yml

@@ -0,0 +1,33 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+  workflow_dispatch:
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v4
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-FreerDPS.opam'
+          custom_image: ${{ matrix.image }}
+
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

.gitignore

@@ -1,11 +1,13 @@
-**/Makefile
-**/Makefile.conf
-**/.CoqMakefile.d
-**/.Makefile.d
+**/Makefile.rocq
+**/Makefile.rocq.conf
+**/.Makefile.rocq.d
 **/*.glob
 **/*.vo
 **/*.vok
 **/*.vos
 **/.*.aux
 _opam
-_build
+_build
+freer_playground/.Makefile.d
+freer_playground/Makefile
+freer_playground/Makefile.conf

Makefile

@@ -0,0 +1,15 @@
+all: Makefile.rocq
+	$(MAKE) -f Makefile.rocq all
+
+clean: Makefile.rocq
+	$(MAKE) -f Makefile.rocq cleanall
+
+Makefile.rocq: _CoqProject
+	rocq makefile -f _CoqProject -o Makefile.rocq
+
+_CoqProject Makefile: ;
+
+%: Makefile.rocq
+	$(MAKE) -f Makefile.rocq $@
+
+.PHONY: all clean

README.md

@@ -1,59 +1,53 @@
-This repo is the home of **FreerDPS**.
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
+# Freer Equational Reasoning for Distributed and Probabilistic Systems
 
-FreerDPS stands for : **Freer** *E*quational *R*easoning for **D**istributed and **P**robabilistic **S**ystems.
+[![Docker CI][docker-action-shield]][docker-action-link]
 
-# Code structure
+[docker-action-shield]: https://github.com/FreerDPS/FreerDPS/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/FreerDPS/FreerDPS/actions/workflows/docker-action.yml
 
-As of now, the code base is mainly a rewrite of [FreeSpec](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect.
 
-# Install
 
-## Libraries
 
-You need to install the following libraries for the project to work :
-- coq 9.0 (it will use rocq as soon as monae makes the move)
-- monae
-- infotheo
-- mathcomp
-- hierarchy builder
+This work started as a rewrite/extension of [FreeSpec Core](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect.
 
-## Commands
+This work has been accepted for presentation to [COMPAS26](https://2026.compas-conference.fr/) (no paper available online).
 
-Mainly for interns installing it first time :
+## Meta
 
-```sh
-opam switch create . ocaml-base-compiler.4.14.2
-eval $(opam env)
-opam pin add coq 9.0.0
-eval $(opam env)
+- Author(s):
+  - Hugo Forraz (initial)
+- License: [MIT License](LICENSE)
+- Additional dependencies:
+  - [MathComp](https://math-comp.github.io)
+  - [MathComp Analysis](https://github.com/math-comp/analysis)
+  - [MathComp Algebra Tactics](https://github.com/math-comp/algebra-tactics)
+  - Monae
+- Related publication(s):
+  - []()
 
-opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq-hierarchy-builder coq-mathcomp-ssreflect coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable coq-mathcomp-classical 
-```
-
-In case monae / infotheo can not be installed through opam, you can clone them from github and fix their versions.
+## Building and installation instructions
 
-Versions known to work :
-- monae : dev
-- infotheo : 0.9.6 => [I have a local fork for now](https://github.com/forrazh/infotheo/tree/fix/0.9.6)
+The easiest way to install the latest released version of Freer Equational Reasoning for Distributed and Probabilistic Systems
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
-You just need to clone the repositories and run : 
-
-```sh
-eval $(opam env) # it should be the same switch as the one created above
-oam pin add .
+```shell
+opam repo add rocq-released https://rocq-prover.org/opam/released
+opam install coq-FreerDPS
 ```
 
-inside the repository.
-
-Once everything is installed, you can run the following commands :
-
-```sh
-coq_makefile -f _CoqProject -o Makefile 
-make
+To instead build and install manually, you need to make sure that all the
+libraries this development depends on are installed.  The easiest way to do that
+is still to rely on opam:
+
+``` shell
+git clone https://github.com/FreerDPS/FreerDPS.git
+cd FreerDPS
+opam repo add rocq-released https://rocq-prover.org/opam/released
+opam install --deps-only .
+make   # or make -j <number-of-cores-on-your-machine>
+make install
 ```
-
-
-# Publications 
-
-This work has been submitted to COMPAS and is under reviewing. 

_CoqProject

@@ -1,15 +1,16 @@
 -Q theories FreerDPS
+
 -arg -w -arg -projection-no-head-constant
 
 ./theories/Component.v
 ./theories/Contract.v
 ./theories/Core.v
+./theories/mathcomp_extra.v
 ./theories/Hoare.v
-./theories/HoareFacts.v
-./theories/Impure.v
+./theories/Freer.v
 ./theories/Init.v
 ./theories/Instrument.v
-./theories/Interface.v
+./theories/Effect.v
 ./theories/Semantics.v
-./theories/Tactics.v
 ./theories/Typeclasses.v
+./examples/airlock.v

coq-FreerDPS.opam

@@ -0,0 +1,34 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "Hugo Forraz"
+version: "dev"
+
+homepage: "https://github.com/FreerDPS/FreerDPS"
+dev-repo: "git+https://github.com/FreerDPS/FreerDPS.git"
+bug-reports: "https://github.com/FreerDPS/FreerDPS/issues"
+license: "MIT"
+
+synopsis: "TODO"
+description: """
+This work started as a rewrite/extension of [FreeSpec Core](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect.
+
+This work has been accepted for presentation to [COMPAS26](https://2026.compas-conference.fr/) (no paper available online)."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq"
+  "rocq-mathcomp-ssreflect" {>= "2.5.0"}
+  "rocq-mathcomp-analysis" {>= "1.16.0"}
+  "coq-mathcomp-algebra-tactics" {>= "1.2.7"}
+  "rocq-monae" {= "0.9.2"}
+]
+
+tags: [
+  "logpath:"
+]
+authors: [
+  "Hugo Forraz"
+]

dune-project

@@ -14,7 +14,7 @@
  (synopsis "A FreeSpec rewrite to bring the power of equational reasoning and probabilities.")
  (description "A longer description")
  (depends 
-    (coq-monae (= "dev"))
+    (coq-monae (= "latest"))
     (coq-equations (="latest"))
     (coq-hierarchy-builder (= "latest"))
     (coq-mathcomp-ssreflect (= "latest"))
@@ -26,10 +26,10 @@
     (coq-mathcomp-classical (= "latest"))
     (coq (= "9.0"))
     (coq-stdlib (= "9.0.0"))
-    (coq-infotheo (= "dev"))
+    (coq-infotheo (= "0.9.7"))
     ))
 
-; monae and infotheo are in dev for now because we want 
+; monae is in dev and infotheo is in 0.9.7 for now because we want 
 ; to use the latest coq version available, which is not 
 ; possible using the current opam versions.