Commit b65f1f51 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Compatibility with Dedukti stable version

parent 2bdca923
......@@ -40,8 +40,52 @@ arithmetic and algebra. It is written in FoCaLiZe\Cite{focalize}, a
language that eases the definition of mathematical structures and the
automation of proofs and for which a translator to Dedukti exists.
* Content of the MathTransfer library
* Installation
The following tools are required to compile the MathTransfer library:
For the core of the library:
- FoCaLiZe version 0.9.2
FoCaLiZe features Dedukti export since version 0.9.2
- Dedukti version 2.5
- Sukerujo version 2.5
Sukerujo is an alternative Dedukti parser used by FoCaLiZe
- Zenon Modulo version 0.4.2
For the interoperability library, the following extra tools are
required to import logical developments from other proof systems:
- Coq version 8.4pl6
Other 8.4 versions of Coq might work as well but Coqine requires Coq
version < 8.5.
- Coqine version 0.4
Coqine is a Coq to Dedukti translator. Previous Coqine versions are
not compatible with Dedukti version >= 2.5.
- OpenTheory version 1.3
OpenTheory is an interoperability format for proof assistants of the
HOL family. The OpenTheory tool is a package manager for files in
this format.
The OpenTheory tool is used to download the OpenTheory standard
library.
- Holide version 0.2.1 Holala
Holide is an OpenTheory to Dedukti translator. The Holala variant
limits the dependencies on non-constructive axioms by taking
implication and universal quantification as primitives.
* Detailed Content of the MathTransfer library
** Core
The core of the MathTransfer library, located in the [[./core][core]] directory
......
......@@ -35,7 +35,8 @@ find_binary () {
echo "$A"
return 0
else
print_to_stderr "program '$1$2' not found"
print_to_stderr ""
print_to_stderr "ERROR: program '$1$2' not found"
return 1
fi
fi
......@@ -67,7 +68,8 @@ find_and_check_binary () {
print_to_file "$3=\"$A\""
return 0
else
print_to_stderr "'$1' has version '$B' but version '$5' was expected"
print_to_stderr ""
print_to_stderr "ERROR: '$1' has version '$B' but version '$5' was expected"
return 1
fi
}
......@@ -76,17 +78,14 @@ echo > .config_vars &&
# Mandatory
find_binary_no_check "dkdep" ".native" "DKDEP" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.6" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.6" &&
find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.6" &&
# find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Meta Sukerujo v2.6" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5" &&
find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.5" &&
find_and_check_binary "focalizec" "" "FOCALIZEC" "-v" "The FoCaLize compiler, version 0.9.2" &&
find_binary_no_check "focalizedep" "" "FOCALIZEDEP" &&
find_binary_no_check "dktactics" "" "DKTACTICS" &&
find_and_check_binary "coqc" "" "COQC" "-v | grep version | cut -d ' ' -f 6" "8.4pl6" &&
find_and_check_binary "coqtop" "" "COQTOP" "-v | grep version | cut -d ' ' -f 6" "8.4pl6" &&
# Check that Coqine is installed, do not know how to check the version
# Check that Coqine is installed. I do not know how to check the version
if ( echo 'Require Coqine.' | ${VARS["COQTOP"]})
then
print_to_stderr "Coqine found."
......@@ -96,4 +95,6 @@ else
fi &&
find_and_check_binary "opentheory" "" "OPENTHEORY" "-v" "opentheory 1.3 (release 20160204)" &&
find_and_check_binary "holide" "" "HOLIDE" "--version" "Holide HOL to Dedukti translator, version 0.2.1 (Holala)"
find_and_check_binary "holide" "" "HOLIDE" "--version" "Holide HOL to Dedukti translator, version 0.2.1 (Holala)" &&
print_to_stderr "" &&
print_to_stderr "Configuration successful, please invoke make"
......@@ -23,7 +23,7 @@ $(ART_FILES): %.art:
$(OPENTHEORY) info --article -o $@ $*
depend: .depend
.depend: $(ART_FILES:.art=.dk)
.depend:
$(FOCALIZEDEP) $(FCL_FILES) > $@
natural_coq.sk: CoqNaturals.dko
......
......@@ -4,7 +4,7 @@ include ../../Makefile.rules
FCL_FILES=$(wildcard *.fcl)
V_FILES=$(wildcard *.v)
DK_FILES=$(wildcard *.dk)
all: $(FCL_FILES:.fcl=.dko) $(V_FILES:.v=.dko) $(DK_FILES:.dk=.dko)
all: $(FCL_FILES:.fcl=.dko) $(V_FILES:.v=.dko) $(DK_FILES:.dk=.dko) Coq__Init__Datatypes.dko
INCLUDE_DIRS= -I ../../core/logic
......@@ -27,12 +27,18 @@ Coq__Init__Logic.dko : Coq__Init__Logic.dk Coq.dko
Coq__Init__Datatypes.dko : Coq__Init__Datatypes.dk Coq.dko Coq__Init__Logic.dko
Coq__Init__Wf.dko : Coq__Init__Wf.dk Coq.dko Coq__Init__Logic.dko Coq__Init__Datatypes.dko
# Dependencies between the dk/dko files could be automatised as
# $(DKDEP) $(INCLUDE_DIRS) >> $@ but only starting with Dedukti v2.6
# because dkdep v2.5 does not implement the -I option and we need it
# to ignore hol.dko which lies in another directory
Coq.dko: Coq.dk
hol_to_coq.dko: hol_to_coq.dk Coq.dko holtypes.dko
depend: .depend
.depend:
$(FOCALIZEDEP) $(FCL_FILES) > $@
$(DKDEP) $(INCLUDE_DIRS) $(DK_FILES) >> $@
-include .depend
clean :
rm -f *.dko *.sk* *.fo *.vo *.pfc *.zv *.mangled *_fcl.* .depend
rm -f *.dko *.sk* *.fo *.vo *.pfc *.zv *.mangled *_fcl.* Coq__*.dk Dedukti__Coqine.dk *.glob holtypes.dk .depend
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment