Merge branch 'include/comoproj-v2.1.0' into 'main'

Include/comoproj v2.1.0 See merge request !35

Merge branch 'include/comoproj-v2.1.0' into 'main'
087722f5 · Max Ole Elliger · ace951a0 · 5abc71bd · 087722f5 · 087722f5
Commit 087722f5 authored 1 year ago by Max Ole Elliger
--- a/.gitignore
+++ b/.gitignore
@@ -13,5 +13,5 @@ Makefile.coq
 Makefile.coq.conf
 .Makefile.coq.d
 .coq-html.mk
-public/*
+html/*
 _CoqProject
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -2,16 +2,6 @@
 stages:
  - build

-#Use the following lines to compile code in a specific version. You can copy this lines to compile your project based on multiple versions.
-build_8_16_1:
-  image: coqorg/coq:8.16.1
-  stage: build
-  script:
-    - make all
-  artifacts:
-    paths:
-      - public/*
-
 # Compile your project based on latest coq version.
 build_latest:
  image: coqorg/coq:latest

--- a/Makefile
+++ b/Makefile
 # Configuration

 PROJNAME = CoMoEx
-HTMLDIR = public/
 COMPONENTS := prop:PropLogic fol:FOL ind:Induction

 COQDOC_FLAGS = --utf8

-all: coq html _CoqProject
+all: coq html

 coq: Makefile.coq
 	$(MAKE) -f Makefile.coq all

-Makefile.coq: _CoqProject Makefile
-	coq_makefile -f $< -o $@
+html: Makefile.coq
+	$(MAKE) -f Makefile.coq html

-GENERATED_HTML = .coq-html.mk
-clean: Makefile.coq $(SRC)
+Makefile.coq: _CoqProject
+	coq_makefile -f $< -o $@ COQDOCEXTRAFLAGS = "--lib-name $(PROJNAME)"
+
+clean: Makefile.coq
 	$(MAKE) -f $< cleanall
 	rm -f Makefile.coq
 	rm -f Makefile.coq.conf
 	rm -f .Makefile.coq.d
 	rm -f _CoqProject

-clean_html: clean $(HTMLDIR)
-	rm -f $(GENERATED_HTML)
-	rm -f -r $(HTMLDIR)
-
-clean_all: clean clean_html
-
 define GENCoqPr
 BEGIN { RS="[[:space:]]"; FS=":" }\
 {					\
@@ -45,46 +40,4 @@ endef
 _CoqProject: Makefile
 	echo $(COMPONENTS) | awk '$(GENCoqPr)' > $@

-$(HTMLDIR):
-	mkdir -p $(HTMLDIR)
-
-html: $(HTMLDIR)/toc.html
-
-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
+.PHONY: all coq html clean