-
Notifications
You must be signed in to change notification settings - Fork 18
Expand file tree
/
Copy pathMakefile.coq.conf
More file actions
71 lines (60 loc) · 10.7 KB
/
Makefile.coq.conf
File metadata and controls
71 lines (60 loc) · 10.7 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
# This configuration file was generated by running:
# coq_makefile -f _CoqProject coq/lib_utils/LibUtilsAssoc.v coq/lib_utils/LibUtilsBag.v coq/lib_utils/LibUtilsBindings.v coq/lib_utils/LibUtilsBindingsNat.v coq/lib_utils/LibUtilsClosure.v coq/lib_utils/LibUtilsCompat.v coq/lib_utils/LibUtilsCoqLibAdd.v coq/lib_utils/LibUtilsDigits.v coq/lib_utils/LibUtilsFresh.v coq/lib_utils/LibUtilsGroupByDomain.v coq/lib_utils/LibUtilsInterleaved.v coq/lib_utils/LibUtilsLattice.v coq/lib_utils/LibUtilsLift.v coq/lib_utils/LibUtilsLiftIterators.v coq/lib_utils/LibUtilsListAdd.v coq/lib_utils/LibUtilsResult.v coq/lib_utils/LibUtilsSortingAdd.v coq/lib_utils/LibUtilsStringAdd.v coq/lib_utils/LibUtilsSublist.v coq/lib_utils/LibUtils.v coq/CertRL/LM/R_compl.v coq/CertRL/LM/check_sub_structure.v coq/CertRL/LM/compatible.v coq/CertRL/LM/continuous_linear_map.v coq/CertRL/LM/fixed_point.v coq/CertRL/LM/hierarchyD.v coq/CertRL/LM/hilbert.v coq/CertRL/LM/linear_map.v coq/CertRL/LM/logic_tricks.v coq/CertRL/LM/lax_milgram.v coq/CertRL/LM/lax_milgram_cea.v coq/utils/BasicUtils.v coq/utils/Assoc.v coq/utils/ClassicUtils.v coq/utils/CoquelicotAdd.v coq/utils/ELim_Seq.v coq/utils/ExtrFloatishIEEE.v coq/utils/improper_integrals.v coq/utils/Isomorphism.v coq/utils/ListAdd.v coq/utils/FiniteType.v coq/utils/FiniteTypeVector.v coq/utils/NumberIso.v coq/utils/PairEncoding.v coq/utils/Quotient.v coq/utils/quotient_space.v coq/utils/RealAdd.v coq/utils/RbarAdd.v coq/utils/RiemannAdd.v coq/utils/StreamAdd.v coq/utils/StreamLimits.v coq/utils/Sums.v coq/utils/nvector.v coq/utils/Vector.v coq/utils/PushNeg.v coq/utils/DVector.v coq/utils/Utils.v coq/utils/Floatish/FloatishDef.v coq/utils/Floatish/FloatishOps.v coq/utils/Floatish/FloatishRealOps.v coq/utils/Floatish/FloatishInterval.v coq/utils/Floatish/FloatishIEEE.v coq/utils/Floatish/FloatishReal.v coq/utils/Floatish.v coq/NeuralNetworks/AxiomaticNormedRealVectorSpace.v coq/NeuralNetworks/DefinedFunctions.v coq/NeuralNetworks/derivlemmas.v coq/NeuralNetworks/Gen_NN.v coq/ProbTheory/Almost.v coq/ProbTheory/BorelSigmaAlgebra.v coq/ProbTheory/DiscreteProbSpace.v coq/ProbTheory/Dynkin.v coq/ProbTheory/Event.v coq/ProbTheory/Independence.v coq/ProbTheory/ProbSpace.v coq/ProbTheory/FunctionsToReal.v coq/ProbTheory/Measures.v coq/ProbTheory/RandomVariable.v coq/ProbTheory/RealRandomVariable.v coq/ProbTheory/RandomVariableFinite.v coq/ProbTheory/RandomVariableL2.v coq/ProbTheory/RandomVariableLpNat.v coq/ProbTheory/RandomVariableLpR.v coq/ProbTheory/RandomVariableLinf.v coq/ProbTheory/OrthoProject.v coq/ProbTheory/RealVectorHilbert.v coq/ProbTheory/SimpleExpectation.v coq/ProbTheory/ConditionalExpectation.v coq/ProbTheory/Expectation.v coq/ProbTheory/RbarExpectation.v coq/ProbTheory/VectorConditionalExpectation.v coq/ProbTheory/SigmaAlgebras.v coq/ProbTheory/VectorRandomVariable.v coq/ProbTheory/Martingale.v coq/ProbTheory/MartingaleConvergence.v coq/ProbTheory/MartingaleStopped.v coq/ProbTheory/Gaussian.v coq/ProbTheory/ProductSpace.v coq/ProbTheory/ProductSpaceDep.v coq/CertRL/pmf_monad.v coq/CertRL/qvalues.v coq/CertRL/mdp.v coq/CertRL/mdp_turtle.v coq/CertRL/finite_time.v coq/CertRL/cond_expt.v coq/CertRL/pmf_prob.v coq/QLearn/Dvoretzky.v coq/QLearn/Bellman.v coq/QLearn/qlearn_aux.v coq/QLearn/qlearn.v coq/QLearn/qlearn_redux.v coq/QLearn/infprod.v coq/QLearn/sumtest.v coq/QLearn/slln.v coq/QLearn/vecslln.v coq/QLearn/uniform_converge.v coq/QLearn/lim_add.v coq/QLearn/Tsitsiklis.v coq/QLearn/jaakkola_vector.v coq/FHE/nth_root.v coq/FHE/encode.v coq/FHE/encrypt.v coq/FHE/zp_prim_root.v coq/FHE/arith.v coq/API.v -o Makefile.coq
COQBIN?=
ifneq (,$(COQBIN))
# add an ending /
COQBIN:=$(COQBIN)/
endif
COQMKFILE ?= "$(COQBIN)coq_makefile"
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_CMDLINE_VFILES := coq/lib_utils/LibUtilsAssoc.v coq/lib_utils/LibUtilsBag.v coq/lib_utils/LibUtilsBindings.v coq/lib_utils/LibUtilsBindingsNat.v coq/lib_utils/LibUtilsClosure.v coq/lib_utils/LibUtilsCompat.v coq/lib_utils/LibUtilsCoqLibAdd.v coq/lib_utils/LibUtilsDigits.v coq/lib_utils/LibUtilsFresh.v coq/lib_utils/LibUtilsGroupByDomain.v coq/lib_utils/LibUtilsInterleaved.v coq/lib_utils/LibUtilsLattice.v coq/lib_utils/LibUtilsLift.v coq/lib_utils/LibUtilsLiftIterators.v coq/lib_utils/LibUtilsListAdd.v coq/lib_utils/LibUtilsResult.v coq/lib_utils/LibUtilsSortingAdd.v coq/lib_utils/LibUtilsStringAdd.v coq/lib_utils/LibUtilsSublist.v coq/lib_utils/LibUtils.v coq/CertRL/LM/R_compl.v coq/CertRL/LM/check_sub_structure.v coq/CertRL/LM/compatible.v coq/CertRL/LM/continuous_linear_map.v coq/CertRL/LM/fixed_point.v coq/CertRL/LM/hierarchyD.v coq/CertRL/LM/hilbert.v coq/CertRL/LM/linear_map.v coq/CertRL/LM/logic_tricks.v coq/CertRL/LM/lax_milgram.v coq/CertRL/LM/lax_milgram_cea.v coq/utils/BasicUtils.v coq/utils/Assoc.v coq/utils/ClassicUtils.v coq/utils/CoquelicotAdd.v coq/utils/ELim_Seq.v coq/utils/ExtrFloatishIEEE.v coq/utils/improper_integrals.v coq/utils/Isomorphism.v coq/utils/ListAdd.v coq/utils/FiniteType.v coq/utils/FiniteTypeVector.v coq/utils/NumberIso.v coq/utils/PairEncoding.v coq/utils/Quotient.v coq/utils/quotient_space.v coq/utils/RealAdd.v coq/utils/RbarAdd.v coq/utils/RiemannAdd.v coq/utils/StreamAdd.v coq/utils/StreamLimits.v coq/utils/Sums.v coq/utils/nvector.v coq/utils/Vector.v coq/utils/PushNeg.v coq/utils/DVector.v coq/utils/Utils.v coq/utils/Floatish/FloatishDef.v coq/utils/Floatish/FloatishOps.v coq/utils/Floatish/FloatishRealOps.v coq/utils/Floatish/FloatishInterval.v coq/utils/Floatish/FloatishIEEE.v coq/utils/Floatish/FloatishReal.v coq/utils/Floatish.v coq/NeuralNetworks/AxiomaticNormedRealVectorSpace.v coq/NeuralNetworks/DefinedFunctions.v coq/NeuralNetworks/derivlemmas.v coq/NeuralNetworks/Gen_NN.v coq/ProbTheory/Almost.v coq/ProbTheory/BorelSigmaAlgebra.v coq/ProbTheory/DiscreteProbSpace.v coq/ProbTheory/Dynkin.v coq/ProbTheory/Event.v coq/ProbTheory/Independence.v coq/ProbTheory/ProbSpace.v coq/ProbTheory/FunctionsToReal.v coq/ProbTheory/Measures.v coq/ProbTheory/RandomVariable.v coq/ProbTheory/RealRandomVariable.v coq/ProbTheory/RandomVariableFinite.v coq/ProbTheory/RandomVariableL2.v coq/ProbTheory/RandomVariableLpNat.v coq/ProbTheory/RandomVariableLpR.v coq/ProbTheory/RandomVariableLinf.v coq/ProbTheory/OrthoProject.v coq/ProbTheory/RealVectorHilbert.v coq/ProbTheory/SimpleExpectation.v coq/ProbTheory/ConditionalExpectation.v coq/ProbTheory/Expectation.v coq/ProbTheory/RbarExpectation.v coq/ProbTheory/VectorConditionalExpectation.v coq/ProbTheory/SigmaAlgebras.v coq/ProbTheory/VectorRandomVariable.v coq/ProbTheory/Martingale.v coq/ProbTheory/MartingaleConvergence.v coq/ProbTheory/MartingaleStopped.v coq/ProbTheory/Gaussian.v coq/ProbTheory/ProductSpace.v coq/ProbTheory/ProductSpaceDep.v coq/CertRL/pmf_monad.v coq/CertRL/qvalues.v coq/CertRL/mdp.v coq/CertRL/mdp_turtle.v coq/CertRL/finite_time.v coq/CertRL/cond_expt.v coq/CertRL/pmf_prob.v coq/QLearn/Dvoretzky.v coq/QLearn/Bellman.v coq/QLearn/qlearn_aux.v coq/QLearn/qlearn.v coq/QLearn/qlearn_redux.v coq/QLearn/infprod.v coq/QLearn/sumtest.v coq/QLearn/slln.v coq/QLearn/vecslln.v coq/QLearn/uniform_converge.v coq/QLearn/lim_add.v coq/QLearn/Tsitsiklis.v coq/QLearn/jaakkola_vector.v coq/FHE/nth_root.v coq/FHE/encode.v coq/FHE/encrypt.v coq/FHE/zp_prim_root.v coq/FHE/arith.v coq/API.v
COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES))
COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES))
COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES))
COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES))
COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES))
COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES))
COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES))
COQMF_METAFILE =
###############################################################################
# #
# Path directives (-I, -R, -Q). #
# #
###############################################################################
COQMF_OCAMLLIBS =
COQMF_SRC_SUBDIRS =
COQMF_COQLIBS = -R coq FormalML
COQMF_COQLIBS_NOML = -R coq FormalML
COQMF_CMDLINE_COQLIBS =
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_COQLIB=/Users/bmt/.opam/default/lib/coq/
COQMF_COQCORELIB=/Users/bmt/.opam/default/lib/coq/../coq-core/
COQMF_DOCDIR=/Users/bmt/.opam/default/share/doc/
COQMF_OCAMLFIND=/Users/bmt/.opam/default/bin/ocamlfind
COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
COQMF_WARN=-warn-error +a-3
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
COQMF_COQ_NATIVE_COMPILER_DEFAULT=no
COQMF_WINDRIVE=
###############################################################################
# #
# Native compiler. #
# #
###############################################################################
COQMF_COQPROJECTNATIVEFLAG =
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
COQMF_OTHERFLAGS = '-set' 'Warnings=+default,-ambiguous-path,-coercions,-hiding-delimiting-key,-overwriting-delimiting-key,-redundant-canonical-projection,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden'
COQMF_INSTALLCOQDOCROOT = FormalML