math-comp · gares · Jun 10, 2021 · Jun 9, 2021 · Jun 9, 2021 · Jun 9, 2021
diff --git a/coq/.gitignore b/coq/.gitignore
@@ -1,4 +1,7 @@
-ch*.html
-index.html
+*.html
+*.vok
+*.vos
+*.glob
+*.aux
 package-lock.json
 node_modules
diff --git a/coq/Makefile b/coq/Makefile
@@ -1,30 +1,47 @@
 files=ch0.v  ch1.v  ch2.v  ch3.v  ch4.v  ch6.v  ch7_1.v ch7_2.v ch7_3.v ch7_4.v ch7_5.v  ch8.v
 
-all: $(files:%.v=%.html) index.html
+all: check $(files:%.v=%.html) index.html
+
+check:
 	for f in $(files); do coqc $$f || exit 1; done
 
 ch%.html: ch%.v
-	cat jscoq_header.html > $@
+	cat jscoq_header.htpl > $@
 	echo "<h1>Chapter $*</h1><div><textarea id='coq-code'>" >> $@
 	cat $< >> $@
 	echo >> $@
 	echo "</textarea></div>" >> $@
 	echo "<script type='text/javascript'>" >> $@
 	echo "var coqdoc_ids = ['coq'];" >> $@
 	echo "</script>" >> $@
-	cat jscoq_footer.html >> $@
+	cat jscoq_footer.htpl >> $@
 
-index.html:
-	cat index_header.html > $@
+chapters.txt:
 	for file in $(files) ; do \
-		echo -n "<a href=\"" >> $@ ; \
 		echo -n $$file | sed "s/\.v/\.html/" >> $@ ; \
-		echo -n "\">" >> $@ ; \
-                echo -n "Chapter " >> $@ ; \
-                echo -n $$file | sed "s/\.v//" >> $@ ; \
-                echo "</a><br> " >> $@ ; \
+                echo -n "@@@" >> $@ ; \
+                echo $$file | sed "s/^ch//" | sed "s/\.v//" >> $@ ; \
 	done
-	cat index_footer.html >> $@
 
-clean:
-	rm -f $(files:%.v=%.html) index.html
+chapterlist.html: chapters.txt
+	awk -F@@@ '{printf "<a href=\"%s\">Chapter %s</a><br>\n", $$1, $$2}' $^ > $@
+
+	# echo > $@
+	# for line in $(files) ; do \
+	# 	echo -n "<a href=\"" >> $@ ; \
+	# 	echo -n $$file | sed "s/\.v/\.html/" >> $@ ; \
+	# 	echo -n "\">" >> $@ ; \
+        #         echo -n "Chapter " >> $@ ; \
+        #         echo -n $$file | sed "s/\.v//" >> $@ ; \
+        #         echo "</a><br> " >> $@ ; \
+	# done
+
+index.html: chapterlist.html
+	cat index.htpl | sed '/-*- CHAPTER_LIST -*-/r chapterlist.html' > $@
+
+clean: cclean
+	rm -f $(files:%.v=%.html) chapters.txt chapterlist.html index.html
+
+# clean compilation artifacts
+cclean:
+	rm -f $(files:%.v=%.vo) $(files:%.v=%.vok) $(files:%.v=%.vos) $(files:%.v=.%.aux) $(files:%.v=%.glob)
diff --git a/coq/README.md b/coq/README.md
@@ -1,12 +1,15 @@
 # The "Mathematical Components" book code listings for jsCoq.
 
-Code snippets are intended to be viewed using jsCoq, but you also can just open
-selected `.v` file in your favorite Galina code editor. To view pages in your 
-browser locally you need install `coq`, `mathcomp`, then do `npm install` and
-`node app.js` to run node applicaion (app.js) and then open link 
+Code snippets are intended to be viewed using jsCoq (actual version is
+<a href="https://math-comp.github.io/snippets">here</a>), but you also can just
+open selected `.v` file in your favorite Galina code editor. To view pages in 
+your browser locally you need install `coq`, `mathcomp`, then do `npm install` 
+and `node app.js` to run node applicaion (app.js) and then open link 
 http://127.0.0.1:8010/ in your browser. A bit more detailed instructions are 
 provided below.
 
+You can view jscoq snippets <a href="https://math-comp.github.io/snippets">here</a>.
+
 ## Installation & Run
 
 ### Prerequisites

diff --git a/coq/index.htpl b/coq/index.htpl
@@ -0,0 +1,14 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml">
+  <head>
+    <meta http-equiv="content-type" content="text/html;charset=utf-8" />
+    <title>These are available mathcomp book code listrings by chapters</title>
+  </head>
+
+  <body>
+    <h1>These are available mathcomp book code listings by chapters</h1>
+    <div class="listings-container">
+    <!-- -*- CHAPTER_LIST -*- -->
+    </div>
+  </body>
+</html>
diff --git a/coq/index_footer.html b/coq/index_footer.html
diff --git a/coq/index_header.html b/coq/index_header.html
diff --git a/coq/jscoq_footer.html → coq/jscoq_footer.htpl b/coq/jscoq_footer.html → coq/jscoq_footer.htpl
diff --git a/coq/jscoq_footer_old.html b/coq/jscoq_footer_old.html
diff --git a/coq/jscoq_header.html → coq/jscoq_header.htpl b/coq/jscoq_header.html → coq/jscoq_header.htpl
diff --git a/coq/jscoq_header_old.html b/coq/jscoq_header_old.html
diff --git a/docs/.gitignore b/docs/.gitignore
@@ -0,0 +1,3 @@
+chapterlist.html
+chapters.txt
+snippets/chapterlist.html
diff --git a/docs/Makefile b/docs/Makefile
@@ -1,22 +1,33 @@
-all: book.pdf jscoq coq artwork revision
+all: book.pdf index.html artwork revision
 
 .PHONY: revision
 revision:
 	sed 's/<!--date-->.*/<!--date-->(last update $(shell date))/' -i index.html
 
-jscoq:
-	git clone https://github.com/ejgallego/jscoq-builds.git --depth 1 jscoq
-	git checkout c219bd7e4b207846a607ce5a19513412d826ce7a
-
 book.pdf:
 	make -C ../tex all && cp ../tex/book.pdf .
 
+index.html: chapterlist.html
+	cat index.htpl | sed '/-*- CHAPTER_LIST -*-/r chapterlist.html' > $@
+
+chapterlist.html: chapters.txt
+	awk -F@@@ '{printf "<a href=\"snippets/%s\">Chapter %s</a><br>\n", $$1, $$2}' $^ > $@
+
+chapters.txt: coq
+	cp ../coq/chapters.txt .
+
 coq:
-	make -C ../coq && cp ../coq/ch*.html .
+	make -C ../coq && cp -r ../coq/ch*.html ../coq/index.html ../coq/node_modules snippets
 
 artwork:
 	cp ../artwork/cover/cover-front-web.png .
 
-clean:
-	rm book.pdf ch*.html cover-front-web.png
+iclean:
+	rm -f index.html chapterlist.html chapters.txt
+
+sclean:
+	rm -rf snippets
+	mkdir snippets
 
+clean: iclean sclean
+	rm book.pdf cover-front-web.png
diff --git a/docs/README.md b/docs/README.md
@@ -1 +1,14 @@
 Here are the sources of the [website](https://math-comp.github.io/mcb/) of the book
+
+## Updating index.html
+To update index.html one needs to update index.htpl and then type 
+`make index.html`.
+
+After updating snippets in folder ../coq/ one needs type `make iclean` to clean
+up index-related files, then `make sclean` to clean up the `snippets/`
+directory, and then `make index.html` to generate new index.html. Then one 
+needs to commit the changes including `index.htpl`, `index.html`, and
+the `snippets/` directory.
+
+To update all parts of the index.html file one needs type 
+`make clean && make all`.
diff --git a/docs/ch0.html b/docs/ch0.html
diff --git a/docs/ch3.html b/docs/ch3.html