From ee67c5069c35395f601373e44a2902ec85fd8a24 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Sat, 9 Dec 2023 18:08:09 +0100
Subject: [PATCH] artifact generation

---
 artifact-clean/INSTRUCTIONS.md | 30 ++++++++++++++++++++++++++++++
 artifact-clean/Makefile        |  8 ++++++++
 artifact-clean/coq-elpi        |  1 +
 make_artifact.sh               | 16 ++++++++++++++++
 4 files changed, 55 insertions(+)
 create mode 100644 artifact-clean/INSTRUCTIONS.md
 create mode 100644 artifact-clean/Makefile
 create mode 160000 artifact-clean/coq-elpi
 create mode 100755 make_artifact.sh

diff --git a/artifact-clean/INSTRUCTIONS.md b/artifact-clean/INSTRUCTIONS.md
new file mode 100644
index 0000000..a8b4a4d
--- /dev/null
+++ b/artifact-clean/INSTRUCTIONS.md
@@ -0,0 +1,30 @@
+# Trocq
+
+0. We use the Opam package manager, please install it from the
+   official Opam webpage: https://opam.ocaml.org/doc/Install.html
+
+1. Create a fresh Opam switch (development was done with
+   OCaml 4.12.0, but anything newer should work). An existing switch may
+   also be used, if:
+   - the version the `coq` package is at least 8.17 and
+   - the `coq-hott` packaged is either not installed or at version 8.17 and
+   - package `coq-elpi` is **not** installed.
+
+   The plugin indeed requires a custom version of Coq-Elpi, with features
+   related to universe polymorphism that are still experimental. This
+   is why a version of the Coq-Elpi sources is included in this
+   artifact.
+
+2. Install Trocq and its dependencies by running `make` in the root
+   directory of the archive.
+
+3. Open your IDE at the root of the `trocq` directory. Open and execute
+   any of the example files present in the `trocq/examples` directory.
+
+   The examples have been put inside the `trocq` project for the sake of
+   convenience, so that the `-noinit`  and `-indices-matter` options of `coqtop` are taken into account in the IDE.
+
+   Please use either:
+   - CoqIDE (available in your switch via `opam install coqide`)
+   - VSCode or VSCodium with the **VSCoq Legacy** extension.
+   - emacs together with proof-general
\ No newline at end of file
diff --git a/artifact-clean/Makefile b/artifact-clean/Makefile
new file mode 100644
index 0000000..9ea3227
--- /dev/null
+++ b/artifact-clean/Makefile
@@ -0,0 +1,8 @@
+.PHONY: all
+
+all:
+	opam install ./coq-elpi
+	opam install ./trocq
+
+clean:
+	opam uninstall coq-elpi coq-trocq
\ No newline at end of file
diff --git a/artifact-clean/coq-elpi b/artifact-clean/coq-elpi
new file mode 160000
index 0000000..8cb61ed
--- /dev/null
+++ b/artifact-clean/coq-elpi
@@ -0,0 +1 @@
+Subproject commit 8cb61ede0077079129f08801f13023b3d93b5d20
diff --git a/make_artifact.sh b/make_artifact.sh
new file mode 100755
index 0000000..264c54e
--- /dev/null
+++ b/make_artifact.sh
@@ -0,0 +1,16 @@
+#!/bin/sh
+rm -rf artifact-clean/trocq artifact-clean/coq-elpi
+git clone -b strat --depth 1 https://github.com/ecranceMERCE/coq-elpi/ artifact-clean/coq-elpi
+rm theories/.*.aux theories/*.glob theories/*.vo theories/*.vok theories/*.vos
+mkdir artifact-clean/trocq/
+mkdir artifact-clean/trocq/theories
+mkdir artifact-clean/trocq/examples
+cp theories/*.v artifact-clean/trocq/theories/
+cp examples/*.v artifact-clean/trocq/examples/
+rm -f artifact-clean/trocq/theories/Inductives.v
+rm -f artifact-clean/trocq/examples/list_to_seq.v
+cp -R elpi artifact-clean/trocq/elpi
+cp _CoqProject artifact-clean/trocq/
+cp Makefile artifact-clean/trocq/
+cp coq-trocq.opam artifact-clean/trocq/
+zip -u -r artifact-clean artifact-clean