From 42480310c63d1c31cb54484d29c7ceb592d662ef Mon Sep 17 00:00:00 2001 From: Benedikt Ahrens Date: Thu, 8 Dec 2016 22:11:42 +0100 Subject: [PATCH] reorganizing the repository --- .gitignore | 18 ++ Make | 19 -- Makefile | 22 +- .dir-locals.el => Modules/.dir-locals.el | 2 +- Modules/Prelims/.package/files | 4 + ardef.v => Modules/Prelims/ardef.v | 2 +- modules.v => Modules/Prelims/modules.v | 0 .../Prelims/quotientfunctor.v | 0 uniproof.v => Modules/Prelims/uniproof.v | 6 +- build/CoqMakefile.make | 304 ------------------ build/Makefile-configuration-template | 30 ++ 11 files changed, 68 insertions(+), 339 deletions(-) create mode 100644 .gitignore delete mode 100644 Make rename .dir-locals.el => Modules/.dir-locals.el (81%) create mode 100644 Modules/Prelims/.package/files rename ardef.v => Modules/Prelims/ardef.v (99%) rename modules.v => Modules/Prelims/modules.v (100%) rename quotientfunctor.v => Modules/Prelims/quotientfunctor.v (100%) rename uniproof.v => Modules/Prelims/uniproof.v (98%) delete mode 100644 build/CoqMakefile.make create mode 100644 build/Makefile-configuration-template diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..7d97fe5 --- /dev/null +++ b/.gitignore @@ -0,0 +1,18 @@ +/build/Makefile-coq.make.bak +/TAGS* +/html +/enhanced-html +/build/Makefile-configuration +/.coq_makefile_input +/.coq_makefile_output +/build/CoqMakefile.make +/latex/*.log +/latex/*.aux +/latex/*.pdf +/latex/*.tex +/latex/*.out +/latex/*.bbl +/latex/*.blg +/latex/*.fdb_latexmk +/latex/*.fls +/latex/coqdoc.sty diff --git a/Make b/Make deleted file mode 100644 index bfc55d5..0000000 --- a/Make +++ /dev/null @@ -1,19 +0,0 @@ -# -*- makefile-gmake -*- - -# DO NOT EDIT THIS FILE! -# It is made by automatically (by code in Makefile) - --R TypeTheory/TypeTheory/ TypeTheory --R UniMath/UniMath/ UniMath --Q . Largecat - -modules.v -mylibtactics.v -quotientfunctor.v -ardef.v -uniproof.v - - -# Local Variables: -# compile-command: "coq_makefile -f .coq_makefile_input -o CoqMakefile.make.tmp && mv CoqMakefile.make.tmp build/CoqMakefile.make" -# End: diff --git a/Makefile b/Makefile index 755acc6..9c28b71 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,7 @@ endif endif ############################################ # The packages, listed in order by dependency: -#PACKAGES += Auxiliary +PACKAGES += Prelims #PACKAGES += ALV1 #PACKAGES += Displayed_Cats #PACKAGES += ALV2 @@ -39,7 +39,7 @@ COQDOC := coqdoc COQDOCFLAGS := -interpolate --charset utf-8 COQDOC_OPTIONS := -toc $(COQDOCFLAGS) $(COQDOCLIBS) -utf8 -PACKAGE_FILES := $(patsubst %, TypeTheory/%/.package/files, $(PACKAGES)) +PACKAGE_FILES := $(patsubst %, Modules/%/.package/files, $(PACKAGES)) ifneq "$(INCLUDE)" "no" include build/CoqMakefile.make @@ -95,15 +95,15 @@ COQDEFS := --language=none \ -r "/^[[:space:]]*Notation.* \"'\([[:alnum:]]+\)'/\1/" \ -r '/^[[:space:]]*Tactic Notation.* "\([[:alnum:]]+\)" /\1/' -# $(foreach P,$(PACKAGES),$(eval TAGS-$P: $(filter TypeTheory/$P/%,$(VFILES)); etags -o $$@ $$^)) +# $(foreach P,$(PACKAGES),$(eval TAGS-$P: $(filter Modules/$P/%,$(VFILES)); etags -o $$@ $$^)) $(VFILES:.v=.vo) : # $(COQBIN)coqc # TAGS : $(PACKAGE_FILES) $(VFILES); etags $(COQDEFS) $(VFILES) FILES_FILTER := grep -vE '^[[:space:]]*(\#.*)?$$' -$(foreach P,$(PACKAGES),$(eval $P: $(shell B be a function. It induces an equivalence relation on A. diff --git a/build/CoqMakefile.make b/build/CoqMakefile.make deleted file mode 100644 index 0f7a0c1..0000000 --- a/build/CoqMakefile.make +++ /dev/null @@ -1,304 +0,0 @@ -############################################################################# -## v # The Coq Proof Assistant ## -## $@ - printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/Largecat && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "Largecat" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT) \\\n' >> "$@" - printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find $(INSTALLDEFAULTROOT)/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - chmod +x $@ - -uninstall: uninstall_me.sh - sh $< - -.merlin: - @echo 'FLG -rectypes' > .merlin - @echo "B $(COQLIB) kernel" >> .merlin - @echo "B $(COQLIB) lib" >> .merlin - @echo "B $(COQLIB) library" >> .merlin - @echo "B $(COQLIB) parsing" >> .merlin - @echo "B $(COQLIB) pretyping" >> .merlin - @echo "B $(COQLIB) interp" >> .merlin - @echo "B $(COQLIB) printing" >> .merlin - @echo "B $(COQLIB) intf" >> .merlin - @echo "B $(COQLIB) proofs" >> .merlin - @echo "B $(COQLIB) tactics" >> .merlin - @echo "B $(COQLIB) tools" >> .merlin - @echo "B $(COQLIB) toplevel" >> .merlin - @echo "B $(COQLIB) stm" >> .merlin - @echo "B $(COQLIB) grammar" >> .merlin - @echo "B $(COQLIB) config" >> .merlin - -clean:: - rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES) - find . -name .coq-native -type d -empty -delete - rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) - rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex - - rm -rf html mlihtml uninstall_me.sh - -cleanall:: clean - rm -f $(patsubst %.v,.%.aux,$(VFILES)) - -archclean:: - rm -f *.cmx *.o - -printenv: - @"$(COQBIN)coqtop" -config - @echo 'CAMLC = $(CAMLC)' - @echo 'CAMLOPTC = $(CAMLOPTC)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' - @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' - -.coq_makefile_output: Make - mv -f $@ $@.bak - "$(COQBIN)coq_makefile" -f $< -o $@ - - -################### -# # -# Implicit rules. # -# # -################### - -$(VOFILES): %.vo: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $< - -$(GLOBFILES): %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $< - -$(VFILES:.v=.vio): %.vio: %.v - $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< - -$(GFILES): %.g: %.v - $(GALLINA) $< - -$(VFILES:.v=.tex): %.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -$(HTMLFILES): %.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -$(VFILES:.v=.g.tex): %.g.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -$(GHTMLFILES): %.g.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ - -$(addsuffix .d,$(VFILES)): %.v.d: %.v - $(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -$(addsuffix .beautified,$(VFILES)): %.v.beautified: - $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v - -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING - diff --git a/build/Makefile-configuration-template b/build/Makefile-configuration-template new file mode 100644 index 0000000..9f90669 --- /dev/null +++ b/build/Makefile-configuration-template @@ -0,0 +1,30 @@ +# -*- makefile-gmake -*- + +# To configure the makefile, copy this file (Makefile-configuration-template) +# to Makefile-configuration (in this directory) and then edit it. Do not edit +# this file, for it is just a template, and you might accidentally check it in. +# The first thing to change, when editing this file, is to remove this comment. + +# To remove the configurations, it is best to delete all the text in your copy +# of this file, rather than removing the file, so the timestamp on the newly +# empty file will trigger "make" to remake the files that depend on the +# configuration. + +# The Boolean values are "yes" and "no". + +############################################################################# + +# Whether to build coq by checking out the appropriate git repository and compiling +# it with ocamlc and gcc: +BUILD_COQ = yes + +# When coq is being built, whether also to build coqide. +BUILD_COQIDE = no + +# When BUILD_COQ is "no", give the path to the coq binary "coqtop", including the +# final "/" (if nonempty), unless it is on the PATH: +COQBIN = + +# List here any packages you'd like to try to build on a test basis. +# When the packages work, add them to the list in ../Makefile. +PACKAGES =