Merge branch 'ci'

.github/workflows/pvs_prelude.yml

+name: pvs_prelude
+
+on: [push]
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v2
+
+    - name: setup
+      run: ci/bootstrap.sh
+      shell: sh
+
+    - name: install personoj
+      run: |
+        eval $(opam env --switch=~/lambdapi --set-switch)
+        bmake -C encoding install
+        sed "s:PVSDKPATH:$(pwd):" pvs-load.lisp > ~/.pvs.lisp
+        cat ~/.pvs.lisp
+
+    - name: translate and typecheck
+      run: |
+        eval $(opam env --switch=~/lambdapi --set-switch)
+        cd pvs-translation-tools/prelude || exit 1
+        # Comment out theories that consume too much memory during 
+        # typechecking
+        sed -i 's/^floor_ceil$/-floor_ceil/' theories
+        sed -i 's/^modulo_arithmetic$/-modulo_arithmetic/' theories
+        sed -i 's/^mod$/-mod/' theories
+        bmake PVSPATH=~/PVS # Set in bootstrap.sh

ci/bootstrap.sh

+#!/bin/sh
+set -eu
+
+curl -s 'http://www.lsv.fr/~hondet/pvs/lambdapi-pvs_1.0_all.deb' > lambdapi-pvs.deb 
+yes | sudo apt-get -q install ./lambdapi-pvs.deb
+yes | sudo apt-get install -q emacs # For PVS
+sudo sysctl kernel.unprivileged_userns_clone=1 
+yes '/usr/local/bin' | sudo bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.1.0"
+
+url="https://downloads.sourceforge.net/project/sbcl/sbcl/1.4.16/sbcl-1.4.16-x86-64-linux-binary.tar.bz2"
+(cd "${HOME}" || exit 1
+ curl "$url" -L | tar jx
+ ln -s sbcl* sbcl)
+
+opam init --bare --no-setup -q
+
+gclone () {
+    (cd "$HOME"
+     git clone "$1"
+     (cd "$2" || exit 1
+      git checkout "$3"))
+}
+
+gclone https://github.com/gabrielhdt/lambdapi.git lambdapi aae26f2d
+gclone https://github.com/SRI-CSL/PVS.git PVS pvs7.1
+
+(cd "${HOME}/lambdapi" || exit 1
+ opam switch create . --locked --deps-only --yes
+ eval "$(opam env)"
+ make install
+ why3 config detect)
+
+(cd "${HOME}/PVS" || exit 1
+ autoconf
+ ./configure)
+
+ EMACS="$(command -v emacs)"
+ SBCLISP_HOME="${HOME}/sbcl"
+ PVSPATH="${HOME}/PVS"
+ export PVSPATH
+
+ for p in $(find pvs-translation-tools/prelude_patches -name '*.diff' | sort); do
+     patch "${PVSPATH}/lib/prelude.pvs" "$p"
+ done
+
+ (cd "${PVSPATH}"
+  make EMACS="$EMACS" SBCLISP_HOME="$SBCLISP_HOME" >output 2>&1)

pvs-load.lisp

@@ -2,4 +2,4 @@
 
 (defparameter *pvs-dedukti-path* "PVSDKPATH")
 (dolist (m '("utils" "packages" "dklog" "dk-sig" "dk-recursive" "pp-dk3" "pvs"))
-  (load (concatenate 'string *pvs-dedukti-path* m ".lisp")))
+  (load (concatenate 'string *pvs-dedukti-path* "/exporter/" m ".lisp")))

pvs-translation-tools/prelude/theories

@@ -71,17 +71,17 @@ floor_ceil
 euclidean_division
 divides
 modulo_arithmetic
-subrange_inductions
+-subrange_inductions # FIXME: Ill formed application (term is not typed in PVS)
 bounded_int_inductions
 bounded_nat_inductions
-subrange_type
-int_types
-nat_types
+-subrange_type # Overloading on dependent types needed
+-int_types # Overloading on dependent types
+-nat_types # Overloading on dependent types
 nat_fun_props
-finite_sets
-restrict_set_props
-extend_set_props
-function_image_aux
+-finite_sets # Depends on nat_types
+-restrict_set_props # Depends on finite_sets
+-extend_set_props # Depends on finite_sets
+-function_image_aux # Depends on finite_sets
 -function_iterate # Recursive function definition
 sequences
 seq_functions
@@ -94,8 +94,8 @@ seq_functions
 -lex4 # Depends on ordinals
 -list # Is a datatype
 -list_props # Recursive function
-map_props
-more_map_props
+-map_props # Depends on list
+-more_map_props # Must depend on map_props or list
 -filters # Recursive functions
 -list2finseq # Depends on list
 -list2set # Recursive functions, depends on list
@@ -105,16 +105,16 @@ more_map_props
 -lift # Is a datatype
 -union # Datatype
 mucalculus
-ctlops
-fairctlops
+-ctlops # Seem to mess with K_conversion
+-fairctlops # Mess with K_conversion
 -Fairctlops # Recursive functions
-bit
-bv
+-bit # FIXME: subtyping failure
+-bv # Depedns on bit
 -exp2 # Recursive functions
-bv_concat_def
-bv_bitwise
+-bv_concat_def # depends on bit
+-bv_bitwise # depedns on bit
 -bv_nat # Recursive
-empty_bv
+-empty_bv # Depends on bit
 -bv_caret # Dependent tuple (I think)
 mod
 -bv_arith_nat_defs # May depend on bv_caret
@@ -126,11 +126,11 @@ mod
 -finite_sets_of_sets # Recursive functions
 EquivalenceClosure
 QuotientDefinition
-KernelDefinition
-QuotientKernelProperties
-QuotientSubDefinition
-QuotientExtensionProperties
-QuotientDistributive
-QuotientIteration
+-KernelDefinition # FIXME: Unification failure
+-QuotientKernelProperties # Depeds on KernelDefinition
+-QuotientSubDefinition # depends on QuotientSubDefinition
+-QuotientExtensionProperties # depends on KernelDefinition
+-QuotientDistributive # Depends on previous theories
+-QuotientIteration # Depends on previous theories
 -PartialFunctionDefinitions # Contains a record
 -PartialFunctionComposition # Depends on previous thy

pvs-translation-tools/prelude/theories.patch

-diff --git a/translations/prelude/theories b/translations/prelude/theories
-index f239adab..f38a6056 100644
---- a/translations/prelude/theories
-+++ b/translations/prelude/theories
-@@ -65,23 +65,23 @@ real_props
- extra_real_props
- extra_tegies
- rational_props
--integer_props
-+-integer_props # FIXME
- floor_ceil
- -exponentiation # Contains a recursive function definition
- euclidean_division
--divides
--modulo_arithmetic
--subrange_inductions
-+-divides # FIXME: Last declaration fails
-+-modulo_arithmetic # Very long to typecheck
-+-subrange_inductions # FIXME: Ill formed application (term is not typed in PVS)
- bounded_int_inductions
- bounded_nat_inductions
--subrange_type
--int_types
--nat_types
-+-subrange_type # Overloading on dependent types needed
-+-int_types # Overloading on dependent types
-+-nat_types # Overloading on dependent types
- nat_fun_props
--finite_sets
--restrict_set_props
--extend_set_props
--function_image_aux
-+-finite_sets # Depends on nat_types
-+-restrict_set_props # Depends on finite_sets
-+-extend_set_props # Depends on finite_sets
-+-function_image_aux # Depends on finite_sets
- -function_iterate # Recursive function definition
- sequences
- seq_functions
-@@ -94,8 +94,8 @@ seq_functions
- -lex4 # Depends on ordinals
- -list # Is a datatype
- -list_props # Recursive function
--map_props
--more_map_props
-+-map_props # Depends on list
-+-more_map_props # Must depend on map_props or list
- -filters # Recursive functions
- -list2finseq # Depends on list
- -list2set # Recursive functions, depends on list
-@@ -105,18 +105,18 @@ more_map_props
- -lift # Is a datatype
- -union # Datatype
- mucalculus
--ctlops
--fairctlops
-+-ctlops # Seem to mess with K_conversion
-+-fairctlops # Mess with K_conversion
- -Fairctlops # Recursive functions
--bit
--bv
-+-bit # FIXME: subtyping failure
-+-bv # Depedns on bit
- -exp2 # Recursive functions
--bv_concat_def
--bv_bitwise
-+-bv_concat_def # depends on bit
-+-bv_bitwise # depedns on bit
- -bv_nat # Recursive
--empty_bv
-+-empty_bv # Depends on bit
- -bv_caret # Dependent tuple (I think)
--mod
-+-mod # Out of memory
- -bv_arith_nat_defs # May depend on bv_caret
- -bv_int_defs # May depend on bv_caret
- -bv_arithmetic_defs # Recursive functions
-@@ -126,11 +126,11 @@ mod
- -finite_sets_of_sets # Recursive functions
- EquivalenceClosure
- QuotientDefinition
--KernelDefinition
--QuotientKernelProperties
--QuotientSubDefinition
--QuotientExtensionProperties
--QuotientDistributive
--QuotientIteration
-+-KernelDefinition # FIXME: Unification failure
-+-QuotientKernelProperties # Depeds on KernelDefinition
-+-QuotientSubDefinition # depends on QuotientSubDefinition
-+-QuotientExtensionProperties # depends on KernelDefinition
-+-QuotientDistributive # Depends on previous theories
-+-QuotientIteration # Depends on previous theories
- -PartialFunctionDefinitions # Contains a record
- -PartialFunctionComposition # Depends on previous thy