diff --git a/.gitignore b/.gitignore index 6514860712fe52e0b1b5ce6c69491b7a34402bba..395ad7ae13832745adac0f59ba265f3f92f08a14 100644 --- a/.gitignore +++ b/.gitignore @@ -12,5 +12,6 @@ lia.cache Makefile.coq Makefile.coq.conf .Makefile.coq.d +.coq-html.mk public/* _CoqProject diff --git a/Makefile b/Makefile index 19ac4e00fbb3825772d9fec83c0b65f98ea518c0..293a22c27a89559ce60966942b8a20de433e7c1f 100644 --- a/Makefile +++ b/Makefile @@ -1,49 +1,90 @@ -SRC := src -MODULES := IntroElim \ - Laws \ - SomeExamples \ - Induction \ - Forall \ - Exists \ - Groups -LIB := CoMoEx -HTML := public - -VS := $(MODULES:%=$(SRC)/%.v) +# Configuration -.PHONY: all html coq clean clean_html clean_all +PROJNAME = CoMoEx +HTMLDIR = public/ +COMPONENTS := prop:PropLogic fol:FOL ind:Induction -all: coq html _CoqProject +COQDOC_FLAGS = --utf8 -html: coq $(SRC) - mkdir -p public - coqdoc -R $(SRC) $(LIB) $(VS) -d $(HTML) \ - -utf8 --lib-name File --toc +all: coq html _CoqProject coq: Makefile.coq $(MAKE) -f Makefile.coq all -clean: $(SRC) - rm -f $(SRC)/*.vo - rm -f $(SRC)/*.vok - rm -f $(SRC)/*.vos - rm -f $(SRC)/*.glob - rm -f $(SRC)/.*.aux +Makefile.coq: _CoqProject Makefile + coq_makefile -f $< -o $@ + +GENERATED_HTML = .coq-html.mk +clean: Makefile.coq $(SRC) + $(MAKE) -f $< cleanall rm -f Makefile.coq rm -f Makefile.coq.conf rm -f .Makefile.coq.d rm -f _CoqProject -clean_html: clean - rm -f -r $(HTML) +clean_html: clean $(HTMLDIR) + rm -f $(GENERATED_HTML) + rm -f -r $(HTMLDIR) clean_all: clean clean_html -$(SRC): - mkdir -p $(SRC) +define GENCoqPr +BEGIN { RS="[[:space:]]"; FS=":" }\ +{ \ + dirname = $$1; \ + libname = $$2; \ + print "-R " dirname " " libname; \ + find = "find " dirname " -name '*.v' -maxdepth 1"; \ + while ((find | getline) > 0) { \ + print; \ + } \ + close(find); \ +} +endef _CoqProject: Makefile - echo "-R $(SRC) $(LIB)\n\n$(SRC)" > _CoqProject + echo $(COMPONENTS) | awk '$(GENCoqPr)' > $@ + +$(HTMLDIR): + mkdir -p $(HTMLDIR) + +html: $(HTMLDIR)/toc.html -Makefile.coq: Makefile $(VS) $(SRC) - @coq_makefile -o Makefile.coq -R $(SRC) $(LIB) $(VS) +define GENIndex +BEGIN { \ + print "<html><body><h1>Table of Contents for $(PROJNAME)</h1>"; \ +}\ +{\ + printf("<h2><a href=\"%s.html\">%s</a></h2>\n", $$1, $$1);\ +} +endef + +$(HTMLDIR)/toc.html: $(HTMLDIR) + find $(HTMLDIR) -name '*.html' -print0 | xargs -0 basename -a -s .html | grep -Fxv 'toc' | sort | awk '$(GENIndex)' > $@ + +define GENMakefile +BEGIN { RS="[[:space:]]"; FS=":" } \ +{ \ + dirname = $$1; \ + libname = $$2; \ + find = "find " dirname " -name '*.v' -maxdepth 1"; \ + while ((find | getline line) > 0) { \ + match(line, /\/([^\/]+).v/, part); \ + html = HTMLDIR libname "." part[1] ".html"; \ + print html ": " line " " HTMLDIR; \ + print "\tcoqdoc -o $$@ $$< --lib-name $(PROJNAME) $(COQDOC_FLAGS)";\ + htmls = htmls " " html; \ + } \ + close(find); \ +} \ +END { \ + print "html:" htmls; \ + print HTMLDIR "/toc.html: " htmls; \ +} +endef + +$(GENERATED_HTML): Makefile $(HTMLDIR) + echo $(COMPONENTS) | awk -v HTMLDIR="$(HTMLDIR)" '$(GENMakefile)' > $@ +-include $(GENERATED_HTML) + +.PHONY: all html coq clean clean_html clean_all diff --git a/src/Exists.v b/fol/Exists.v similarity index 100% rename from src/Exists.v rename to fol/Exists.v diff --git a/src/Forall.v b/fol/Forall.v similarity index 100% rename from src/Forall.v rename to fol/Forall.v diff --git a/src/Groups.v b/fol/Groups.v similarity index 100% rename from src/Groups.v rename to fol/Groups.v diff --git a/src/Induction.v b/ind/Induction.v similarity index 100% rename from src/Induction.v rename to ind/Induction.v diff --git a/src/IntroElim.v b/prop/IntroElim.v similarity index 100% rename from src/IntroElim.v rename to prop/IntroElim.v diff --git a/src/Laws.v b/prop/Laws.v similarity index 100% rename from src/Laws.v rename to prop/Laws.v diff --git a/src/SomeExamples.v b/prop/SomeExamples.v similarity index 98% rename from src/SomeExamples.v rename to prop/SomeExamples.v index 99b6c5e30b0aac5599542b452d9754cd4bb27cdd..d3584517827d29211659876a3eec133c3194c608 100644 --- a/src/SomeExamples.v +++ b/prop/SomeExamples.v @@ -3,7 +3,7 @@ Require Import Classical_Prop. (** In diesem File habe ich versucht, eigene Beispiele zu kreieren. Wahrscheinlich wird insbesondere diese Sammlung mit der Zeit weiter ergänzt. **) (** Dank der folgenden Zeile stehen uns die bereits bewiesenen Gesetze aus Laws.v zur Verfügung: *) -From CoMoEx Require Import Laws. +From PropLogic Require Import Laws. (** Man kann z.B. `de_morgan_1` ganz normal aufrufen, wie in der folgenden Section zu sehen ist: *)