Merge remote-tracking branch 'dk/main' into spec

.github/workflows/main.yml

@@ -12,7 +12,7 @@ jobs:
         camlp5-version: [8.02.01]
         dedukti-version: [2.7]
         lambdapi-version: [master]
-        dune-version: [3.7.0]
+        dune-version: [3.14.2]
     runs-on: ubuntu-latest
     steps:
     # actions/checkout must be done BEFORE avsm/setup-ocaml
@@ -43,22 +43,25 @@ jobs:
         run: |
           eval `opam env`
           export HOL2DK_DIR=`pwd`
+          export HOLLIGHT_DIR=`pwd`/hol-light
           git clone https://github.com/jrh13/hol-light
           cd hol-light
           git checkout c153f40da8deb3bcc7aaef39126ad15e4713e68c
-          export HOLLIGHT_DIR=`pwd`
           make
           hol2dk patch
       - name: Dump proofs
         run: |
           eval `opam env`
+          export HOL2DK_DIR=`pwd`
+          export HOLLIGHT_DIR=`pwd`/hol-light
           cp xci.ml hol-light/
           cd hol-light
           hol2dk dump-simp-use xci.ml
       - name: Test single-threaded dk output
         run: |
           eval `opam env`
           export HOL2DK_DIR=`pwd`
+          export HOLLIGHT_DIR=`pwd`/hol-light
           cd hol-light
           ln -s ../theory_hol.dk
           hol2dk xci.dk
@@ -67,6 +70,7 @@ jobs:
         run: |
           eval `opam env`
           export HOL2DK_DIR=`pwd`
+          export HOLLIGHT_DIR=`pwd`/hol-light
           cd hol-light
           hol2dk xci.lp
           ln -s ../theory_hol.lp
@@ -76,6 +80,7 @@ jobs:
         run: |
           eval `opam env`
           export HOL2DK_DIR=`pwd`
+          export HOLLIGHT_DIR=`pwd`/hol-light
           cd hol-light
           hol2dk mk 3 xci
           make -f xci.mk -j3 dk
@@ -84,6 +89,7 @@ jobs:
         run: |
           eval `opam env`
           export HOL2DK_DIR=`pwd`
+          export HOLLIGHT_DIR=`pwd`/hol-light
           cd hol-light
           make -f xci.mk -j3 lp
           make -f xci.mk -j3 lpo

Makefile

@@ -216,8 +216,16 @@ nothing:
 
 .PHONY: vo
 vo: $(LP_FILES:%.lp=%.vo)
+ifeq ($(PROGRESS),1)
+	rm -f .finished
+	$(HOL2DK_DIR)/progress &
+endif
 ifneq ($(INCLUDE_VO_MK),1)
 	$(MAKE) INCLUDE_VO_MK=1 vo
+<<<<<<< HEAD
+=======
+	touch .finished
+>>>>>>> dk/main
 endif
 
 COQC_OPTIONS = -no-glob # -w -coercions

TODO.md

@@ -3,6 +3,8 @@ TODO
 
 - generate spec files in ocaml to optimize dependencies (spec files should not depend on abbreviations)
 
+- write progress in an ocaml program, and estimate time wrt size of files
+
 - use a single term_abbrev file for each theorem, and split it
 
 - pre-compute once and for all the type and term variables of axioms and definitions

dune

@@ -5,7 +5,7 @@
 )
 
 (install
- (files coq.v _CoqProject lambdapi.pkg theory_hol.dk theory_hol.lp encoding.lp renaming.lp erasing.lp fusion.ml bool.ml equal.ml xnames.ml patch unpatch add-links Makefile dep-lpo dep-vo README.md)
+ (files coq.v _CoqProject lambdapi.pkg theory_hol.dk theory_hol.lp encoding.lp renaming.lp erasing.lp fusion.ml bool.ml equal.ml xnames.ml patch unpatch add-links Makefile dep-lpo dep-vo progress README.md)
  (section share)
  (package hol2dk)
 )

progress

@@ -0,0 +1,112 @@
+#!/bin/sh
+
+sleep_time=60
+stms=`expr $sleep_time \* 1000`
+
+debug=0
+
+log() {
+    if test $debug -eq 1; then echo "$1"; fi
+}
+
+# total number of coq files to check
+v=`find . -name '*.v' | wc -l`
+log v=$v
+
+# total number of coq files checked
+prevo=0
+
+# current time in seconds
+t0=`date +%s`
+log t0=$t0
+
+hm() {
+    predebug=$debug
+    debug=0
+    log hm
+    m=`expr $1 / 60`
+    log m=$m
+    h=`expr $m / 60`
+    log h=$h
+    m=`expr $m \% 60`
+    echo ${h}h${m}m
+    debug=$predebug
+}
+
+chk() {
+    log chk
+
+    if test -f .finished; then exit; fi
+
+    # total nb of v files checked
+    vo=`find . -name '*.vo' | wc -l`
+    log vo=$vo
+
+    # exit if all v files are compiled
+    if test $vo -eq $v; then exit; fi
+
+    # % of checked files
+    pvo=`expr 100 \* $vo`
+    log pvo=$pvo
+    p=`expr $pvo / $v`
+    log p=$p
+
+    # current time in seconds
+    t=`date +%s`
+    log t=$t
+
+    # elapsed time from the beginning in seconds
+    dt=`expr $t - $t0`
+    log dt=$dt
+
+    # nb of remaining files to check
+    rv=`expr $v - $vo`
+    log rv=$rv
+
+    # nb of v files checked since last chk 
+    dvo=`expr $vo - $prevo`
+    log dvo=$dvo
+
+    if test $dvo -eq 0
+    then
+
+    # elapsed time from the beginning in milliseconds
+    dtms=`expr $dt \* 1000`
+    log dtms=$dtms
+
+    # average elapsed time by file since the beginning in milliseconds
+    if test $vo -eq 0; then exit; fi
+    tvms=`expr $dtms / $vo`
+    log tvms=$tvms
+
+    # remaining time in milliseconds according to average since beginning
+    rtms=`expr $rv \* $tvms`
+    log rtms=$rtms
+
+    else
+
+    # average elapsed time by file since last chk in milliseconds
+    tvms=`expr $stms / $dvo`
+
+    # remaining time in milliseconds according to average since last chk
+    rtms=`expr $rv \* $tvms`
+    log rtms=$rtms
+
+    fi
+
+    # remaining time in seconds according to average since beginning
+    rt=`expr $rtms / 1000`
+    log rt=$rt
+
+    echo '--------------------------------------------------------------------'
+    echo "$vo files ($p%) in `hm $dt`, remaining $rv files and about `hm $rt`"
+    echo '--------------------------------------------------------------------'
+
+    prevo=$vo
+}
+
+while true
+do
+    sleep $sleep_time
+    chk
+done