artifact generation

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

artifact-clean/Makefile

@@ -0,0 +1,8 @@
+.PHONY: all
+
+all:
+	opam install ./coq-elpi
+	opam install ./trocq
+
+clean:
+	opam uninstall coq-elpi coq-trocq

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