Skip to content
Snippets Groups Projects
Unverified Commit 13ff7212 authored by ColinRothgang's avatar ColinRothgang
Browse files

Clean up DHOL prover example build script

parent ff53c8d2
No related branches found
No related tags found
No related merge requests found
......@@ -42,9 +42,6 @@ mathpath archive ../../../../LFX
define dependencies
build MMT/urtheories mmt-omdoc lf.mmt
//build MMT/urtheories mmt-omdoc sequences.mmt
//build MMT/urtheories mmt-omdoc primitive_types/bool.mmt
//build MMT/urtheories mmt-omdoc primitive_types/nat.mmt
build MMT/LATIN2 mmt-omdoc fundamentals/concepts.mmt
build MMT/LATIN2 mmt-omdoc fundamentals/base_languages.mmt
build MMT/LATIN2 mmt-omdoc fundamentals/equality.mmt
......@@ -59,19 +56,30 @@ define dependencies
// for using inductively-defined types
build MMT/LFX mmt-omdoc TypedHierarchy.mmt
build MMT/examples mmt-omdoc induction/lfxi.mmt
// build MMT/LATIN2 mmt-omdoc logic/fol.mmt
// build MMT/urtheories mmt-omdoc sequences.mmt
// build MMT/urtheories mmt-omdoc primitive_types/bool.mmt
// build MMT/urtheories mmt-omdoc primitive_types/nat.mmt
// build MMT/LATIN2 mmt-omdoc logic/pl.mmt
//build MMT/LATIN2 mmt-omdoc logic/stfol.mmt
//build MMT/LATIN2 mmt-omdoc foundations/mizar.mmt
//build MMT/LATIN2 mmt-omdoc foundations/mizar-patterns.mmt
// build MMT/LATIN2 mmt-omdoc logic/fol.mmt
// build MMT/LATIN2 mmt-omdoc logic/stfol.mmt
// build MMT/LATIN2 mmt-omdoc foundations/mizar.mmt
// build MMT/LATIN2 mmt-omdoc foundations/mizar-patterns.mmt
// builds mmt content dependencies of the scala implementation of the prover
// if these are missing run these build commands, then rebuild MMT
build MMT/LATIN2 lf-scala fundamentals/concepts.omdoc
build MMT/LATIN2 mmt-omdoc casestudies/2023-cade/Peano
build MMT/LATIN2 lf-scala fundamentals/base_languages.mmt
build MMT/LATIN2 lf-scala fundamentals/equality.mmt
build MMT/LATIN2 lf-scala logic/fol_like/booleans.mmt
build MMT/LATIN2 lf-scala logic/propositional/pl.mmt
build MMT/LATIN2 lf-scala type_theory/function_types.mmt
build MMT/LATIN2 lf-scala logic/fol_like/sfol.mmt
end
// do dependencies
// build MMT/LATIN2 lf-scala fundamentals/concepts.omdoc
// test DPHOL exporter examples for CADE 2023 paper
build MMT/LATIN2 mmt-omdoc casestudies/2023-cade/
build MMT/LATIN2 tptp casestudies/2023-cade/
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment