aboutsummaryrefslogtreecommitdiff
path: root/coqprime/examples/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'coqprime/examples/Makefile')
-rw-r--r--coqprime/examples/Makefile230
1 files changed, 0 insertions, 230 deletions
diff --git a/coqprime/examples/Makefile b/coqprime/examples/Makefile
deleted file mode 100644
index eff7d0d99..000000000
--- a/coqprime/examples/Makefile
+++ /dev/null
@@ -1,230 +0,0 @@
-#############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.3pl1 ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -f Make -o Makefile
-#
-
-#
-# This Makefile may take 3 arguments passed as environment variables:
-# - COQBIN to specify the directory where Coq binaries resides;
-# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.
-COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g')
-CAMLP4:="$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')"
-ifndef CAMLP4BIN
- CAMLP4BIN:=$(CAMLBIN)
-endif
-
-CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)
-
-##########################
-# #
-# Libraries definitions. #
-# #
-##########################
-
-OCAMLLIBS:=-I .\
- -I ../Tactic\
- -I ../N\
- -I ../Z\
- -I ../PrimalityTest\
- -I ../List\
- -I ../elliptic\
- -I ../num
-COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \
- -I $(COQLIB)/library -I $(COQLIB)/parsing \
- -I $(COQLIB)/pretyping -I $(COQLIB)/interp \
- -I $(COQLIB)/proofs -I $(COQLIB)/tactics \
- -I $(COQLIB)/toplevel \
- -I $(COQLIB)/plugins/cc \
- -I $(COQLIB)/plugins/dp \
- -I $(COQLIB)/plugins/extraction \
- -I $(COQLIB)/plugins/field \
- -I $(COQLIB)/plugins/firstorder \
- -I $(COQLIB)/plugins/fourier \
- -I $(COQLIB)/plugins/funind \
- -I $(COQLIB)/plugins/groebner \
- -I $(COQLIB)/plugins/interface \
- -I $(COQLIB)/plugins/micromega \
- -I $(COQLIB)/plugins/nsatz \
- -I $(COQLIB)/plugins/omega \
- -I $(COQLIB)/plugins/quote \
- -I $(COQLIB)/plugins/ring \
- -I $(COQLIB)/plugins/romega \
- -I $(COQLIB)/plugins/rtauto \
- -I $(COQLIB)/plugins/setoid_ring \
- -I $(COQLIB)/plugins/subtac \
- -I $(COQLIB)/plugins/subtac/test \
- -I $(COQLIB)/plugins/syntax \
- -I $(COQLIB)/plugins/xml
-COQLIBS:=-I .\
- -I ../Tactic\
- -I ../N\
- -I ../Z\
- -I ../PrimalityTest\
- -I ../List\
- -I ../elliptic\
- -I ../num
-COQDOCLIBS:=
-
-##########################
-# #
-# Variables definitions. #
-# #
-##########################
-
-ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
-OPT:=
-COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) -verbose
-ifdef CAMLBIN
- COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)
-endif
-COQC:=$(COQBIN)coqc
-COQDEP:=$(COQBIN)coqdep -c
-GALLINA:=$(COQBIN)gallina
-COQDOC:=$(COQBIN)coqdoc
-COQMKTOP:=$(COQBIN)coqmktop
-CAMLLIB:=$(shell $(CAMLBIN)ocamlc.opt -where)
-CAMLC:=$(CAMLBIN)ocamlc.opt -c -rectypes
-CAMLOPTC:=$(CAMLBIN)ocamlopt.opt -c -rectypes
-CAMLLINK:=$(CAMLBIN)ocamlc.opt -rectypes
-CAMLOPTLINK:=$(CAMLBIN)ocamlopt.opt -rectypes
-GRAMMARS:=grammar.cma
-CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo
-CAMLP4OPTIONS:=
-PP:=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
-
-###################################
-# #
-# Definition of the "all" target. #
-# #
-###################################
-
-VFILES:=BasePrimes.v\
- PocklingtonRefl.v\
- TestLucas.v\
- prime216656403549020227250327256032933021325435259861468456540459488823774358486649614451547405419273433458932168893949521787.v\
- prime329719147332060395689499.v\
- russell1.v\
- russell2.v
-VOFILES:=$(VFILES:.v=.vo)
-VOFILES0:=$(filter-out ,$(VOFILES))
-GLOBFILES:=$(VFILES:.v=.glob)
-VIFILES:=$(VFILES:.v=.vi)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-
-all: $(VOFILES)
-spec: $(VIFILES)
-
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)
-
-all.ps: $(VFILES)
- $(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all-gal.ps: $(VFILES)
- $(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all.pdf: $(VFILES)
- $(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all-gal.pdf: $(VFILES)
- $(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-
-
-####################
-# #
-# Special targets. #
-# #
-####################
-
-.PHONY: all opt byte archclean clean install depend html
-
-%.vo %.glob: %.v
- $(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-%.vi: %.v
- $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
-
-%.g: %.v
- $(GALLINA) $<
-
-%.tex: %.v
- $(COQDOC) -latex $< -o $@
-
-%.html: %.v %.glob
- $(COQDOC) -html $< -o $@
-
-%.g.tex: %.v
- $(COQDOC) -latex -g $< -o $@
-
-%.g.html: %.v %.glob
- $(COQDOC) -html -g $< -o $@
-
-%.v.d: %.v
- $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-byte:
- $(MAKE) all "OPT:=-byte"
-
-opt:
- $(MAKE) all "OPT:=-opt"
-
-install:
- mkdir -p $(COQLIB)/user-contrib
- (for i in $(VOFILES0); do \
- install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \
- install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \
- done)
-
-clean:
- rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~
- rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)
- - rm -rf html
-
-archclean:
- rm -f *.cmx *.o
-
-
-printenv:
- @echo CAMLC = $(CAMLC)
- @echo CAMLOPTC = $(CAMLOPTC)
- @echo CAMLP4LIB = $(CAMLP4LIB)
-
-Makefile: Make
- mv -f Makefile Makefile.bak
- $(COQBIN)coq_makefile -f Make -o Makefile
-
-
--include $(VFILES:.v=.v.d)
-.SECONDARY: $(VFILES:.v=.v.d)
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-30 13:54:48 +0000