Merge pull request #33 from UCSD-PL/develop

Merge in latest changes

.gitmodules

@@ -8,5 +8,172 @@
 	path = dataloader/gestalt-ratio
 	url = https://github.com/HazardousPeach/gestalt-ratio-rust.git
 [submodule "src/coq_serapy"]
-	path = src/coq_serapy
+	path = coq_serapy
 	url = https://github.com/HazardousPeach/coq_serapy.git
+[submodule "coq-projects/coq-procrastination"]
+	path = coq-projects/coq-procrastination
+	url = [email protected]:Armael/coq-procrastination.git
+[submodule "coq-projects/hoare-tut"]
+	path = coq-projects/hoare-tut
+	url = [email protected]:coq-community/hoare-tut.git
+[submodule "coq-projects/zchinese"]
+	path = coq-projects/zchinese
+	url = [email protected]:coq-contribs/zchinese.git
+[submodule "coq-projects/euler-formula"]
+	path = coq-projects/euler-formula
+	url = [email protected]:coq-contribs/euler-formula.git
+	branch = v8.9
+[submodule "coq-projects/UnifySL"]
+	path = coq-projects/UnifySL
+	url = [email protected]:QinxiangCao/UnifySL.git
+[submodule "coq-projects/lemma-overloading"]
+	path = coq-projects/lemma-overloading
+	url = [email protected]:coq-community/lemma-overloading.git
+[submodule "coq-projects/disel"]
+	path = coq-projects/disel
+	url = [email protected]:DistributedComponents/disel.git
+[submodule "coq-projects/algebra"]
+	path = coq-projects/algebra
+	url = [email protected]:coq-contribs/algebra.git
+	branch = v8.9
+[submodule "coq-projects/pocklington"]
+	path = coq-projects/pocklington
+	url = [email protected]:coq-community/pocklington.git
+[submodule "coq-projects/quicksort-complexity"]
+	path = coq-projects/quicksort-complexity
+	url = [email protected]:HazardousPeach/quicksort-complexity.git
+	branch = v8.10
+[submodule "coq-projects/finmap"]
+	path = coq-projects/finmap
+	url = [email protected]:math-comp/finmap.git
+[submodule "coq-projects/coqrel"]
+	path = coq-projects/coqrel
+	url = [email protected]:HazardousPeach/coqrel.git
+	branch = v8.10
+[submodule "coq-projects/twoSquare"]
+	path = coq-projects/twoSquare
+	url = [email protected]:thery/twoSquare.git
+[submodule "coq-projects/QuickChick"]
+	path = coq-projects/QuickChick
+	url = [email protected]:QuickChick/QuickChick.git
+	branch = 8.10
+[submodule "coq-projects/qarith"]
+	path = coq-projects/qarith
+	url = [email protected]:coq-contribs/qarith.git
+	branch = v8.9
+[submodule "coq-projects/pts"]
+	path = coq-projects/pts
+	url = [email protected]:coq-contribs/pts.git
+	branch = v8.9
+[submodule "coq-projects/maths"]
+	path = coq-projects/maths
+	url = [email protected]:coq-contribs/maths.git
+	branch = v8.9
+[submodule "coq-projects/int-map"]
+	path = coq-projects/int-map
+	url = [email protected]:coq-contribs/int-map.git
+	branch = v8.9
+[submodule "coq-projects/ieee754"]
+	path = coq-projects/ieee754
+	url = [email protected]:coq-contribs/ieee754.git
+	branch = v8.9
+[submodule "coq-projects/hardware"]
+	path = coq-projects/hardware
+	url = [email protected]:HazardousPeach/hardware.git
+	branch = v8.10
+[submodule "coq-projects/float"]
+	path = coq-projects/float
+	url = [email protected]:coq-contribs/float.git
+	branch = v8.9
+[submodule "coq-projects/dictionaries"]
+	path = coq-projects/dictionaries
+	url = [email protected]:coq-contribs/dictionaries.git
+	branch = v8.9
+[submodule "coq-projects/buchberger"]
+	path = coq-projects/buchberger
+	url = [email protected]:coq-community/buchberger.git
+	branch = v8.9
+[submodule "coq-projects/bdds"]
+	path = coq-projects/bdds
+	url = [email protected]:coq-contribs/bdds.git
+	branch = v8.10
+[submodule "coq-projects/area-method"]
+	path = coq-projects/area-method
+	url = [email protected]:coq-contribs/area-method.git
+	branch = v8.10
+[submodule "coq-projects/coq"]
+	path = coq-projects/coq
+	url = [email protected]:coq/coq.git
+	branch = v8.10
+[submodule "coq-projects/fcsl-pcm"]
+	path = coq-projects/fcsl-pcm
+	url = [email protected]:imdea-software/fcsl-pcm.git
+[submodule "coq-projects/GeoCoq"]
+	path = coq-projects/GeoCoq
+	url = [email protected]:GeoCoq/GeoCoq.git
+[submodule "coq-projects/coquelicot"]
+	path = coq-projects/coquelicot
+	url = [email protected]:HazardousPeach/coquelicot.git
+[submodule "deps/metalib"]
+	path = deps/metalib
+	url = [email protected]:plclub/metalib.git
+[submodule "coq-projects/additions"]
+	path = coq-projects/additions
+	url = [email protected]:coq-contribs/additions.git
+	branch = v8.9
+[submodule "coq-projects/distributed-reference-counting"]
+	path = coq-projects/distributed-reference-counting
+	url = [email protected]:coq-contribs/distributed-reference-counting.git
+	branch = v8.9
+[submodule "coq-projects/zsearch-trees"]
+	path = coq-projects/zsearch-trees
+	url = [email protected]:coq-contribs/zsearch-trees.git
+[submodule "coq-projects/topology"]
+	path = coq-projects/topology
+	url = [email protected]:coq-community/topology.git
+[submodule "coq-projects/lin-alg-8.10"]
+	path = coq-projects/lin-alg
+	url = [email protected]:HazardousPeach/lin-alg-8.10.git
+[submodule "coq-projects/VST"]
+	path = coq-projects/VST
+	url = [email protected]:HazardousPeach/VST.git
+        branch = v8.10.2
+[submodule "coq-projects/coq-library-undecidability"]
+	path = coq-projects/coq-library-undecidability
+	url = [email protected]:HazardousPeach/coq-library-undecidability.git
+        branch = v8.12.2
+[submodule "coq-projects/fermat4"]
+	path = coq-projects/fermat4
+	url = [email protected]:coq-contribs/fermat4.git
+[submodule "coq-projects/goedel"]
+	path = coq-projects/goedel
+	url = [email protected]:coq-community/goedel.git
+	branch = v8.9
+[submodule "coq-projects/tree-automata"]
+	path = coq-projects/tree-automata
+	url = [email protected]:coq-contribs/tree-automata.git
+	branch = v8.9
+[submodule "coq-projects/verdi"]
+	path = coq-projects/verdi
+	url = [email protected]:uwplse/verdi.git
+[submodule "coq-projects/verdi-raft"]
+	path = coq-projects/verdi-raft
+	url = [email protected]:uwplse/verdi-raft.git
+[submodule "coq-projects/zorns-lemma"]
+	path = coq-projects/zorns-lemma
+	url = [email protected]:coq-community/zorns-lemma.git
+[submodule "coq-projects/math-comp"]
+	path = coq-projects/math-comp
+	url = [email protected]:math-comp/math-comp.git
+[submodule "CompCert"]
+	path = CompCert
+	url = https://github.com/AbsInt/CompCert.git
+[submodule "coq-projects/smc"]
+	path = coq-projects/smc
+	url = [email protected]:dsksh/coq-smc.git
+[submodule "coq-projects/mod-red"]
+	path = coq-projects/mod-red
+	url = [email protected]:coq-contribs/mod-red.git
+[submodule "coq-projects/metalib"]
+	path = coq-projects/metalib
+	url = [email protected]:plclub/metalib.git

Makefile

@@ -3,8 +3,8 @@ SHELL=/usr/bin/env bash
 
 ENV_PREFIX=export LD_LIBRARY_PATH=/usr/local/cuda/lib64/:$$LD_LIBRARY_PATH
 
-NTHREADS=16
-FLAGS=
+NTHREADS?=16
+FLAGS?=
 HIDDEN_SIZE=512
 
 SITE_SERVER=goto
@@ -106,7 +106,7 @@ publish:
 
 publish-weights:
 	rsync -avzP $(WEIGHTSFILE) goto:proverbot9001-site/downloads/weights-`date -I`.dat
-	ssh goto ln -f proverbot9001-site/downloads/weights-`date -I`.dat proverbot9001-site/downloads/weights-latest.dat
+	ssh goto cp proverbot9001-site/downloads/weights-`date -I`.dat proverbot9001-site/downloads/weights-latest.dat
 
 download-weights:
 	curl -o data/polyarg-weights.dat proverbot9001.ucsd.edu/downloads/weights-latest.dat

README.md

@@ -17,7 +17,7 @@ their development headers and pip version.
 If you're running Linux, all three can be generally found in your package repositories.
 If that Linux is ubuntu, you'll have to first run:
 ```
-sudo apt install software-properties-properties
+sudo apt install software-properties-common
 sudo add-apt-repository ppa:avsm/ppa
 sudo apt update
 ```

bench/get_bench_files.sh

@@ -4,4 +4,10 @@ set -e
 
 [ "$#" -ne 1 ] || cd $1
 
+
+if [[ -f configure ]]; then
+    ./configure
+fi
+make -j
+
 comm -12 <(find -name "*.vo" -not -path "./_opam/*" | sed 's/.vo/.v/' | sort) <(find -name "*.v" -not -path "./_opam/*" | sort) > files.txt

beta.txt

@@ -0,0 +1,81 @@
+1.639558813479082694e-02
+-9.827347902182093087e-03
+1.639558813478999774e-02
+2.032676577225059691e-02
+-1.520418449732979533e-03
+2.032676577225082937e-02
+1.639558813479056673e-02
+-9.827347902181409606e-03
+1.639558813479080265e-02
+5.747022772416837157e-03
+-2.402432949342275716e-03
+5.747022772412349427e-03
+-1.119469076024145852e-04
+7.333607981387763389e-03
+-1.119469075976217611e-04
+5.747022772413319137e-03
+-2.402432949344483152e-03
+5.747022772408677017e-03
+1.182680053360825713e-03
+8.550681406945249280e-03
+1.182680053358849213e-03
+-1.112082256926515134e-03
+1.672379721167949543e-02
+-1.112082256927414805e-03
+1.182680053357466421e-03
+8.550681406944300386e-03
+1.182680053357043582e-03
+1.904315467844529611e-02
+1.530891679952701805e-02
+1.904315467844543489e-02
+3.200020007250668763e-02
+4.607745438222393686e-02
+3.200020007251413307e-02
+1.904315467843720883e-02
+1.530891679953733792e-02
+1.904315467844659715e-02
+3.095810389660447193e-02
+1.442646155462873163e-03
+3.095810389659627709e-02
+4.531228937872646551e-02
+3.840710812866048735e-02
+4.531228937872056745e-02
+3.095810389661514742e-02
+1.442646155462898316e-03
+3.095810389659567341e-02
+-7.131974255432099209e-03
+-1.434837993334072900e-02
+-7.131974255433010806e-03
+-1.692629792715076228e-02
+-2.378944853081121566e-02
+-1.692629792714966247e-02
+-7.131974255432646514e-03
+-1.434837993333578157e-02
+-7.131974255432955295e-03
+-9.740081591454200979e-03
+-4.740183760820359214e-03
+-9.740081591455814272e-03
+-1.144880978670498144e-02
+-2.236068453829700986e-02
+-1.144880978670405509e-02
+-9.740081591465839239e-03
+-4.740183760821302904e-03
+-9.740081591467641617e-03
+7.351408369326161915e-03
+1.811027757740975991e-02
+7.351408369344211713e-03
+1.183653789972375497e-02
+4.157524606136539513e-02
+1.183653789971848141e-02
+7.351408369332908255e-03
+1.811027757740401103e-02
+7.351408369329181201e-03
+2.988095657809960656e-02
+1.651687242525414975e-02
+2.988095657809969677e-02
+4.207519337667999654e-02
+5.547979507541279942e-02
+4.207519337667731119e-02
+2.988095657810193109e-02
+1.651687242525474997e-02
+2.988095657809946779e-02

build_coq_projects.sh

@@ -0,0 +1,54 @@
+#!/usr/bin/env bash
+# source swarm-prelude.sh
+
+INIT_CMD="~/opam-scripts/read-opam.sh"
+
+NTHREADS=1
+while getopts ":j:" opt; do
+  case "$opt" in
+    j)
+      NTHREADS="${OPTARG}"
+      ;;
+  esac
+done
+
+# Make sure ruby is in the path
+export PATH=$HOME/.local/bin:$PATH
+
+git submodule init && git submodule update
+
+for project in $(jq -r '.[].project_name' coqgym_projs_splits.json); do
+    SBATCH_FLAGS=""
+
+    echo "#!/usr/bin/env bash" > coq-projects/$project/make.sh
+    echo ${INIT_CMD} >> coq-projects/$project/make.sh
+    if $(jq -e ".[] | select(.project_name == \"$project\") | has(\"build_command\")" \
+         coqgym_projs_splits.json); then
+        BUILD=$(jq -r ".[] | select(.project_name == \"$project\") | .build_command" \
+                   coqgym_projs_splits.json)
+    else
+        BUILD="make"
+    fi
+
+    if $(jq -e ".[] | select(.project_name == \"$project\") | has(\"build_partition\")" \
+            coqgym_projs_splits.json); then
+        PART=$(jq -r ".[] | select(.project_name == \"$project\") | .build_partition" \
+                   coqgym_projs_splits.json)
+        SBATCH_FLAGS+=" -p $PART"
+    fi
+
+    if $(jq -e ".[] | select(.project_name == \"$project\") | has(\"timeout\")" \
+         coqgym_projs_splits.json); then
+        TIMEOUT=$(jq -r ".[] | select(.project_name == \"$project\") | .timeout" \
+                     coqgym_projs_splits.json)
+        SBATCH_FLAGS+=" --time=${TIMEOUT}"
+    fi
+
+    SWITCH=$(jq -r ".[] | select(.project_name == \"$project\") | .switch" coqgym_projs_splits.json)
+
+    echo "eval \"$(opam env --set-switch --switch=$SWITCH)\"" >> coq-projects/$project/make.sh
+
+    echo "$BUILD $@" >> coq-projects/$project/make.sh
+    chmod u+x coq-projects/$project/make.sh
+    (cd coq-projects/$project && sbatch --cpus-per-task=${NTHREADS} $SBATCH_FLAGS -o build-output.out make.sh)
+done