runtimeverification · palmskog · Dec 15, 2023 · Dec 15, 2023 · Dec 15, 2023 · Dec 15, 2023
diff --git a/BUILDING.md b/BUILDING.md
@@ -7,6 +7,7 @@ The guide assumes a Unix shell, and some installation commands
 assume a Debian-like Linux distribution, such as Ubuntu.
 
 - [Building VLSM manually](#building-vlsm-manually)
+- [Building VLSM using the Coq Platform](#building-vlsm-using-the-coq-platform)
 - [Editor instructions](#editor-instructions)
 
 Notes for Windows users:
@@ -92,6 +93,50 @@ cd vlsm
 make -j $(nproc)
 ```
 
+## Building VLSM using the Coq Platform
+
+### Download and unpack the Coq Platform scripts
+
+The latest Coq Platform release is always available using [this link](https://github.com/coq/platform/releases/latest).
+
+However, for the purposes of demonstration, we will assume the archive is called `2023.11.0.zip`.
+
+```shell
+wget https://github.com/coq/platform/archive/refs/tags/2023.11.0.zip
+unzip 2023.11.0.zip
+```
+
+### Run the Platform scripts
+
+```shell
+cd platform-2023.11.0
+./coq_platform_make.sh
+```
+
+### Activate the Platform switch
+
+The Platform scripts will create a new opam switch, whose
+name can be viewed by running `opam switch`. Here, we assume
+the switch is called `__coq-platform.2023.11.0~8.18~2023.11`.
+
+```shell
+opam switch __coq-platform.2023.11.0~8.18~2023.11
+eval $(opam env)
+```
+
+### Clone the project repository
+
+```shell
+git clone https://github.com/runtimeverification/vlsm
+```
+
+### Build the project
+
+```shell
+cd vlsm
+make -j $(nproc)
+```
+
 ## Editor instructions
 
 We recommend using the Visual Studio Code (VS Code) editor, which you can download and install from [here](https://code.visualstudio.com).
@@ -100,19 +145,19 @@ If you are using WSL on Windows, you need to install the VS Code [WSL extension]
 
 We recommend also installing the [Fast Unicode Math Characters extension](https://marketplace.visualstudio.com/items?itemName=GuidoTapia2.unicode-math-vscode), to enable easier input of mathematical symbols.
 
-To enable Coq support in VS Code, there are two options: the VsCoq extension and the Coq LSP extension.
+To enable Coq support in VS Code, there are two options: the VsCoq extension and the Coq LSP extension. Note that these extensions are restricted to Coq 8.18.0 and later. For earlier versions, you can use the [VsCoq Legacy extension](https://github.com/coq-community/vscoq/tree/vscoq1).
 
 ### VsCoq extension
 
-The [VsCoq extension](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq) is a stable standalone extension using Coq's legacy XML protocol. It can be installed from the command line:
+To install the [VsCoq extension](https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp) from the command line, make sure that [switch creation](#install-a-switch-for-opam) and [dependency installation](#install-the-project-dependencies-via-opam) are done and then run:
 
 ```shell
-code --install-extension maximedenes.vscoq
+opam install vscoq-language-server && code --install-extension maximedenes.vscoq
 ```
 
 ## Coq LSP extension
 
-The [Coq LSP extension](https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp) is an experimental new extension with advanced features that requires installing an opam package. To install it from the command line, make sure that [switch creation](#install-a-switch-for-opam) and [dependency installation](#install-the-project-dependencies-via-opam) are done and then run:
+To install the [Coq LSP extension](https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp) from the command line, make sure that [switch creation](#install-a-switch-for-opam) and [dependency installation](#install-the-project-dependencies-via-opam) are done and then run:
 
 ```shell
 opam install coq-lsp && code --install-extension ejgallego.coq-lsp

diff --git a/Makefile.coq.local b/Makefile.coq.local
@@ -45,19 +45,19 @@ DUPLICATES.md: $(DOCVFILES)
 alectryon: $(ALECTRYONHTMLFILES)
 .PHONY: alectryon
 
-# requires https://github.com/palmskog/rvdpdgraph/tree/v8.16
+# requires https://github.com/palmskog/rvdpdgraph/tree/v8.18
 rvdpd: $(SVGFILES)
 .PHONY: rvdpd
 
 $(ALECTRYONHTMLFILES): %.alectryon.html: %.v %.glob %.vo $(ALECTRYONDIR)/toc.html
-	$(SHOW)'ALECTRYON --output-directory $(ALECTRYONDIR) --output $(ALECTRYONDIR)/$(addsuffix .html,$(subst /,.,$(patsubst theories/%,%,$(basename $<))))'
-	$(HIDE)$(ALECTRYON) $(ALECTRYONHTMLFLAGS) $(COQDOCLIBS) --output-directory $(ALECTRYONDIR) --output $(ALECTRYONDIR)/$(addsuffix .html,$(subst /,.,$(patsubst theories/%,%,$(basename $<)))) $<
+	$(SHOW)'ALECTRYON --output-directory $(ALECTRYONDIR) --output $(ALECTRYONDIR)/$(addsuffix .html,$(subst /,.,$(patsubst theories/%,VLSM.%,$(basename $<))))'
+	$(HIDE)$(ALECTRYON) $(ALECTRYONHTMLFLAGS) $(COQDOCLIBS) --output-directory $(ALECTRYONDIR) --output $(ALECTRYONDIR)/$(addsuffix .html,$(subst /,.,$(patsubst theories/%,VLSM.%,$(basename $<)))) $<
 .PHONY: $(ALECTRYONHTMLFILES)
 
 $(ALECTRYONDIR)/toc.html:
 	$(HIDE)mkdir -p $(@D)
 	$(HIDE)cat resources/alectryon_toc_header.html > $@
-	$(HIDE)for vfile in $(subst /,.,$(patsubst theories/%,%,$(basename $(DOCVFILES)))) ; do \
+	$(HIDE)for vfile in $(subst /,.,$(patsubst theories/%,VLSM.%,$(basename $(DOCVFILES)))) ; do \
 	    echo "    <li><a href='$$vfile.html'>$$vfile</a></li>" >> $@; \
 	done
 	$(HIDE)cat resources/alectryon_toc_footer.html >> $@
@@ -71,13 +71,13 @@ $(COQDOCDIR)/map.svg: resources/map.dot
 	$(HIDE)dot -T svg resources/map.dot > $@
 
 $(DPDFILES): %.dpd: %.v %.glob %.vo
-	echo "Set DependGraph File \"$@\". Print FileDependGraph $(patsubst theories.%,%,$(subst /,.,$(basename $@)))." | $(COQTOP) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -require-import-from rvdpdgraph rvdpdgraph -load-vernac-object $(patsubst theories.%,%,$(subst /,.,$(basename $@))) -quiet > /dev/null 2>&1
+	echo "Set DependGraph File \"$@\". Print FileDependGraph $(patsubst theories.%,VLSM.%,$(subst /,.,$(basename $@)))." | $(COQTOP) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -require-import-from rvdpdgraph rvdpdgraph -load-vernac-object $(patsubst theories.%,VLSM.%,$(subst /,.,$(basename $@))) -quiet > /dev/null 2>&1
 
 $(DOTFILES): %.dot: %.dpd
 	rvdpd2dot -graphname rvdpdgraph -o $@ $<
 
 $(SVGFILES): %.svg: %.dot $(COQDOCDIR)/map.svg
-	dot -T svg $< > $(COQDOCDIR)/$(patsubst theories.%,%,$(subst /,.,$@))
+	dot -T svg $< > $(COQDOCDIR)/$(patsubst theories.%,VLSM.%,$(subst /,.,$@))
 .PHONY: $(SVGFILES)
 
 resources/index.html: resources/index.md

diff --git a/README.md b/README.md
@@ -72,7 +72,7 @@ make   # or make -j <number-of-cores-on-your-machine>
 - [VLSMs that Generate Logical Formulas](theories/Examples/Tutorial/Formulas.v): construction of VLSMs corresponding to propositional logic symbols, with their composition having well-formed propositional formulas as valid messages.
 - [VLSMs that Multiply](theories/Examples/Tutorial/Multiply.v): construction of VLSMs that perform arithmetic operations, with their composition having products of powers as valid messages.
 - [Primes Composition of VLSMs](theories/Examples/Tutorial/PrimesComposition.v): construction of an infinite family of VLSMs that multiply and their composition based on primes.
-- [Round-based Asynchronous Muddy Children Puzzle](theories/Examples/Tutorial/MuddyChildrenRounds.v): the [muddy children puzzle](https://plato.stanford.edu/entries/dynamic-epistemic/appendix-B-solutions.html#muddy) as a constrained composition of VLSMs that communicate asynchronously in rounds.
+- [Round-based Asynchronous Muddy Children Puzzle](theories/Examples/Tutorial/MuddyChildrenRounds.v): the [muddy children puzzle](https://plato.stanford.edu/entries/dynamic-epistemic/appendix-B-solutions.html#muddy) as a constrained composition of VLSMs that communicate asynchronously in rounds. For additional background, see the [first](https://www.youtube.com/watch?v=lTNG4HJ7V6U) and [second](https://www.youtube.com/watch?v=1H7kAW26pOA) part of a workshop presentation on the formalization.
 
 ### VLSM application: ELMO
 

diff --git a/meta.yml b/meta.yml
@@ -127,7 +127,7 @@ documentation: |-
   - [VLSMs that Generate Logical Formulas](theories/Examples/Tutorial/Formulas.v): construction of VLSMs corresponding to propositional logic symbols, with their composition having well-formed propositional formulas as valid messages.
   - [VLSMs that Multiply](theories/Examples/Tutorial/Multiply.v): construction of VLSMs that perform arithmetic operations, with their composition having products of powers as valid messages.
   - [Primes Composition of VLSMs](theories/Examples/Tutorial/PrimesComposition.v): construction of an infinite family of VLSMs that multiply and their composition based on primes.
-  - [Round-based Asynchronous Muddy Children Puzzle](theories/Examples/Tutorial/MuddyChildrenRounds.v): the [muddy children puzzle](https://plato.stanford.edu/entries/dynamic-epistemic/appendix-B-solutions.html#muddy) as a constrained composition of VLSMs that communicate asynchronously in rounds.
+  - [Round-based Asynchronous Muddy Children Puzzle](theories/Examples/Tutorial/MuddyChildrenRounds.v): the [muddy children puzzle](https://plato.stanford.edu/entries/dynamic-epistemic/appendix-B-solutions.html#muddy) as a constrained composition of VLSMs that communicate asynchronously in rounds. For additional background, see the [first](https://www.youtube.com/watch?v=lTNG4HJ7V6U) and [second](https://www.youtube.com/watch?v=1H7kAW26pOA) part of a workshop presentation on the formalization.
 
   ### VLSM application: ELMO
 

diff --git a/resources/header.html b/resources/header.html
@@ -16,7 +16,7 @@
 	<script>
 	  if (document.title === "Table of Contents") {
 	      document.write("<a href='map.svg'>File dependency graph</a>");
-	  } else {
+	  } else if (document.title !== "Index") {
               document.write("<a href='" + document.title + ".svg'>" + document.title + " dependency graph</a>");
 	  }
 	</script>

diff --git a/resources/index.md b/resources/index.md
@@ -11,16 +11,22 @@ header-includes:
 ---
 
 <div style="text-align:left"><img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
-[View the project on GitHub](https://github.com/runtimeverification/casper-cbc-proofs)
+<a href="https://github.com/runtimeverification/vlsm">View the project on GitHub</a>
 <img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"></div>
 
 ## About
 
 Welcome to the VLSM project website!
 
-A validating labelled state transition and message production system
-(VLSM) abstractly models a distributed system with faults. This project
-contains a formalization of VLSMs and their theory in the Coq proof assistant.
+The theory of Validating Labelled State transition and Message
+production systems (VLSMs) enables describing and proving properties
+of distributed systems executing in the presence of faults. This
+project contains a formalization of this theory in the Coq proof
+assistant along with several examples of distributed protocols
+modeled and verified using VLSMs, including the ELMO
+(Equivocation-Limited Message Observer) family of message
+validating protocols and the Paxos protocol for crash-tolerant
+distributed consensus.
 
 This is an open source project, licensed under the BSD 3-Clause "New" or "Revised" License.
 
@@ -31,7 +37,7 @@ The latest released version of VLSM can be [downloaded from GitHub](https://gith
 ## Documentation
 
 - [latest coqdoc presentation of the source files](latest/coqdoc/toc.html)
-- [latest Alectryon presentation the source files](latest/alectryon/toc.html)
+- [latest Alectryon presentation of the source files](latest/alectryon/toc.html)
 - [stdpp library](https://gitlab.mpi-sws.org/iris/stdpp)
 
 ## Help
@@ -48,7 +54,7 @@ Report [issues on GitHub](https://github.com/runtimeverification/vlsm/issues).
 - Karl Palmskog
 - Lucas Peña
 - Grigore Roșu
-- Traian Șerbănuță
+- Traian Florin Șerbănuță
 - Ioan Teodorescu
 - Dafina Trufaș
 - Jan Tušil

diff --git a/scripts/dotdeps.sh b/scripts/dotdeps.sh
@@ -1,7 +1,7 @@
 #!/bin/sh
 (echo "digraph interval_deps {" ;
 echo "node [shape=ellipse, style=filled, URL=\"\N.svg\", color=black];";
-coqdep -Q theories/VLSM VLSM $* | sed -e 's,theories/,,g' | sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*[.]v//p' |
+coqdep -Q theories VLSM $* | sed -e 's,theories/,VLSM\.,g' | sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*[.]v//p' |
 while read src dst; do
     color=$(echo "$src" | sed -e 's,VLSM.Lib.*,turquoise,;s,VLSM.Core.*,plum,;s,[A-Z].*,white,')
     echo "\"$src\" [fillcolor=$color];"

diff --git a/theories/Lib/Ctauto.v b/theories/Lib/Ctauto.v
@@ -19,3 +19,6 @@ Tactic Notation "itauto" :=
   itauto auto.
 
 Ltac itautor tac := let t := solve[tac | itauto tac] in itauto t.
+
+(* required for documentation generation *)
+Definition iYC2 := True.
diff --git a/theories/Lib/EquationsExtras.v b/theories/Lib/EquationsExtras.v
@@ -14,3 +14,6 @@ Export Equations.Prop.Logic.
   </a>#.
 *)
 Notation "x 'eq:' p" := (exist _ x p) (only parsing, at level 20).
+
+(* required for documentation generation *)
+Definition iYC2 := True.
diff --git a/theories/Lib/Itauto.v b/theories/Lib/Itauto.v
@@ -32,3 +32,6 @@ Tactic Notation "itauto" :=
   itauto auto.
 
 Ltac itautor tac := let t := solve[tac | itauto tac] in itauto t.
+
+(* required for documentation generation *)
+Definition iYC2 := True.