CI: run λ-box and Rust outputs

.github/workflows/ci.yml

@@ -108,13 +108,17 @@ jobs:
 
     - name: Install Peregrine
       working-directory: peregrine-tool/
-      run: |
-        eval $(opam env) && opam install -j4 ./rocq-peregrine.opam
+      run: eval $(opam env) && opam install -j4 ./rocq-peregrine.opam
+
+    - name: Set up Rust
+      uses: dtolnay/rust-toolchain@v1
+      with:
+        toolchain: 1.85.0
 
     - name: Generate HTML
       run: |
         sudo apt-get install -y pandoc zsh wabt
-        eval $(opam env) && make html
+        eval $(opam env) && make gen run html
 
     - name: Deploy HTML website
       if: github.ref == 'refs/heads/master'

Makefile

@@ -1,4 +1,4 @@
-.PHONY: default build install coq html clean
+.PHONY: default build install coq gen run html clean
 
 default: build
 
@@ -17,6 +17,12 @@ coq:
 	coq_makefile -f _CoqProject -o CoqMakefile
 	make -f CoqMakefile
 
+gen: test
+	make -C test gen
+
+run: test
+	make -C test run
+
 html: test
 	make -C test html
 

test/Agda.css

@@ -62,7 +62,7 @@
 
 /* Tabs */
 [data-tab-info] { display: none; }
-.active[data-tab-info] { display: block; }
+.active[data-tab-info] { display: flex; }
 
 .tabs {
     font-size: 25px;

test/Makefile

@@ -9,7 +9,13 @@ gen:
 	mkdir -p gen/
 	./compile.sh
 
-html: gen
+run: # gen
+	@echo == Evaluating λ-box output ==
+	./runRocq.sh
+	@echo == Running Rust ==
+	./runRust.sh
+
+html: # gen run
 	@echo == Generating HTML ==
 	mkdir -p html/ && cp Agda.css html/
 	-cabal run -- agda2lambox --html --css=Agda.css $(MAIN).agda

test/compile.sh

@@ -1,11 +1,11 @@
 #!/bin/zsh
 
-# PREREQUISITES:
+# PRE:
 #   - generated target files are placed under dist/
 BUILD_DIR=dist
 #   - Peregrine compilation output is placed under gen/
 GEN_DIR=gen
-#   - `peregrine` binary should be available
+#   - `peregrine` command should be available
 
 echo "Compiling λ-box..."
 

test/renderTranslations.sh

@@ -1,16 +1,17 @@
 #!/bin/zsh
 
-# PREREQUISITES:
-#   - generated target files are placed under dist/
+# PRE:
+#   - path to generated λ-box files
 BUILD_DIR=dist
-#   - Peregrine compilation output is placed under gen/
+#   - path to Peregrine compilation output
 GEN_DIR=gen
-#   - Agda generated HTML is placed under html/
+# POST:
+#   - path to Agda generated HTML
 AGDA_HTML_DIR=html
 
 echo "Rendering translations..."
 
-for f in $BUILD_DIR/**/* $GEN_DIR/**/**/*; do
+for f in $BUILD_DIR/* $GEN_DIR/*/*; do
 
   echo " * $f"
   ext=${f##*.}
@@ -23,6 +24,7 @@ for f in $BUILD_DIR/**/* $GEN_DIR/**/**/*; do
     "v") echo "coq";; # alas, pandoc has no coq/rocq syntax-highlighting support
     "rs") echo "rust";;
     "ml"|"sml") echo "ocaml";;
+    "result") echo "";;
     *) echo "$ext";;
   esac)
   echo "\`\`\`$lang" > $mdFn
@@ -82,6 +84,8 @@ for f in $BUILD_DIR/**/**.txt; do
     </div>\
     <div class=\"tabs__tab\" id=\"in_3\" data-tab-info>\
         <embed src=\"$fCoq.html\"/>\
+        <div style=\"font-size:50px;\">\&nbsp; ↪ \&nbsp;</div>\
+        <embed src=\"$fCoq.result.html\"/>\
     </div>\
     <div class=\"tabs__tab\" id=\"out_1\" data-tab-info>\
         <embed src=\"$fWasm.html\"/>\
@@ -97,6 +101,8 @@ for f in $BUILD_DIR/**/**.txt; do
     </div>\
     <div class=\"tabs__tab\" id=\"out_5\" data-tab-info>\
         <embed src=\"$fRust.html\"/>\
+        <div style=\"font-size:50px;\">\&nbsp; ↪ \&nbsp;</div>\
+        <embed src=\"$fRust.result.html\"/>\
     </div>\
     <div class=\"tabs__tab\" id=\"out_6\" data-tab-info>\
         <embed src=\"$fElm.html\"/>\

test/runRocq.sh

@@ -0,0 +1,16 @@
+#!/bin/zsh
+
+# PRE:
+#   - path to agda2lambox compilation output
+#   - `coqc` command should be available
+BUILD_DIR=dist
+
+echo "Running λ-box output..."
+
+cd $BUILD_DIR
+
+for f in *.v; do
+  coqc -R ../../theories Agda2Lambox $f &> $f.result
+done
+
+echo "...done!"

test/runRust.sh

@@ -0,0 +1,45 @@
+#!/bin/zsh
+
+# PRE:
+#   - path to Peregrine compilation output
+GEN_DIR=gen
+#   - `cargo` command should be available
+
+echo "Running Peregrine (Rust) output..."
+
+cd $GEN_DIR/rust
+
+# 1. make everything public
+sed -i -e 's/^fn/pub fn/g' -e 's/^struct/pub struct/g' *.rs
+
+# 2. Create Cargo package
+rustPackage="\
+[package]
+name = \"main\"
+[dependencies]
+bumpalo = \"3.20.1\"
+"
+echo $rustPackage > Cargo.toml
+
+for fn in *.rs; do
+  f=${fn%.*}
+  rustBin="\
+[[bin]]
+name = \"$f\"
+path = \"$f.rs\"
+"
+  echo $rustBin >> Cargo.toml
+
+# 3. Attach an individual main function to each test
+  rustMain="\
+pub fn main() {
+  println!(\"{:?}\", Program::new().${f}_test());
+}
+"
+  echo $rustMain >> $f.rs
+
+# 4. Run and record the result of evaluation
+  cargo run --bin $f &> $f.rs.result
+done
+
+echo "...done!"