Skip to content

Commit

Permalink
Merge pull request #231 from Beluga-lang/pr-update-prop-eq-presup
Browse files Browse the repository at this point in the history
Update prop eq presup
  • Loading branch information
Ailrun authored Sep 30, 2024
2 parents 1829f6b + 8b37077 commit 522b9c6
Show file tree
Hide file tree
Showing 22 changed files with 523 additions and 296 deletions.
8 changes: 8 additions & 0 deletions .github/Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -9,5 +9,13 @@ RUN opam repo add coq-released https://coq.inria.fr/opam/released \
&& opam install coq-equations coq-menhirlib menhir ppx_expect \
&& eval $(opam env)

RUN curl https://gitlab.com/api/v4/projects/4207231/packages/generic/graphviz-releases/12.1.1/graphviz-12.1.1.tar.gz -O \
&& tar -xzf graphviz-12.1.1.tar.gz \
&& cd graphviz-12.1.1 \
&& ./configure \
&& make \
&& sudo make install \
&& rm -rf graphviz-12.1.1.tar.gz graphviz-12.1.1

RUN sudo apt-get update -y -q \
&& DEBIAN_FRONTEND=noninteractive sudo apt-get install -y -q --no-install-recommends pandoc
4 changes: 3 additions & 1 deletion .github/workflows/ci_build.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,9 @@ jobs:
startGroup "Build HTMLs for GitHub pages"
if [[ "${{ env.DOC_DEPLOY }}" == 'true' ]]; then
make coqdoc
make depgraphdoc
mv theories/html html
mv theories/dep.html html/dep.html
cp assets/styling.css html/styling.css
cp -r assets/images html/images
pandoc README.md -H assets/include.html --no-highlight --metadata pagetitle='McLTT: A Bottom-up Approach to Implementing A Proof Assistant' -t html --css styling.css -o html/index.html
Expand All @@ -104,7 +106,7 @@ jobs:
run: sudo chown -R 1001:116 .

- name: Deploy GitHub pages
uses: JamesIves/[email protected].4
uses: JamesIves/[email protected].8
if: ${{ success() && env.DOC_DEPLOY == 'true' }}
with:
branch: gh-pages
Expand Down
13 changes: 8 additions & 5 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,12 +1,11 @@
# Dune outputs
_build
*.opam

# Ignore generated parser code
**/parser.ml
**/parser.mli
# Generated coq files
theories/**/Parser.v

# Remove Coq compiled code
# Coq compiler outputs
*.vo
*.glob
*.d
Expand All @@ -21,6 +20,10 @@ CoqMakefile.mk*
*.log
theories/html/

# Editor related
# Generated coq dependency graph
dep.dot
dep.html

# Editor related files
## Emacs
*.~undo-tree~
5 changes: 4 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
.PHONY: all pretty-timed test coqdoc clean
.PHONY: all pretty-timed test coqdoc clean depgraphdoc

all:
@$(MAKE) -C theories
Expand All @@ -11,6 +11,9 @@ pretty-timed:
coqdoc:
@${MAKE} coqdoc -C theories

depgraphdoc:
@$(MAKE) depgraphdoc -C theories

clean:
@$(MAKE) clean -C theories
@dune clean
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ elementary) and serves as a basis for future extensions.

## Online Documentation

We have generated a [Coqdoc](toc.html) for browsing our Coq proof.
We have generated a [Coqdoc](https://beluga-lang.github.io/McLTT/dep.html) for browsing our Coq proof.

## Architecture

Expand Down
4 changes: 2 additions & 2 deletions assets/extra/header.html
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="resources/coqdoc.css" rel="stylesheet" type="text/css" />
<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="resources/config.js"></script>
<script type="text/javascript" src="resources/coqdocjs.js"></script>
</head>
Expand All @@ -20,7 +20,7 @@
<span class="right">
<a href="./">Project Page</a>
<a href="./indexpage.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
<a href="./dep.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
Expand Down
1 change: 0 additions & 1 deletion assets/extra/resources/coqdocjs.css
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,6 @@ html, body {
padding-bottom: 2em;
margin-left: auto;
margin-right: auto;
max-width: 60em;
flex: 1 0 auto;
}

Expand Down
2 changes: 1 addition & 1 deletion assets/extra/resources/coqdocjs.js
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,7 @@ function repairDom(){
function fixTitle(){
var url = "/" + window.location.pathname;
var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.'));
if (basename === "toc") {document.title = "Table of Contents";}
if (basename === "dep") {document.title = "Table of Contents";}
else if (basename === "indexpage") {document.title = "Index";}
else {document.title = basename;}
}
Expand Down
26 changes: 26 additions & 0 deletions assets/extra/resources/depgraph.css
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
svg.depgraph {
max-width: 100%;
}

svg.depgraph > text:first-of-type {
font-weight: bold;
}

.text-highlight-edges text {
opacity: 1 !important;
stroke-width: 3;
font-weight: bold;
fill: indigo;
}

.edge-highlight path {
opacity: 1;
stroke-width: 3;
stroke: blue;
}

.edge-highlight polygon {
opacity: 1;
stroke-width: 3;
stroke: blue;
}
47 changes: 47 additions & 0 deletions assets/extra/resources/depgraph.js
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
function makeEdgesInteractive(evt) {
let svg = evt.target;
let viewBox = svg.viewBox.baseVal;
let edges = document.getElementsByClassName('edge');

Array.from(edges).forEach((edge) => {
edge.addEventListener('click', clickEdge);
});

function clickEdge() {
let edge = this;
if (edge.classList.contains("edge-highlight")) {
edge.classList.remove("edge-highlight");
edge.classList.remove("text-highlight-edges");
} else {
edge.classList.add("edge-highlight");
edge.classList.add("text-highlight-edges");
animateEdge(edge);
}
}

function animateEdge(edge) {
let path = edge.querySelector('path');
let polygon = edge.querySelector('polygon');
let width = viewBox.width;
let length = path.getTotalLength();
let timeUnit = length / width;
// Clear any previous transition
path.style.transition = path.style.WebkitTransition = 'none';
// Set up the starting positions
path.style.strokeDasharray = length + ' ' + length;
path.style.strokeDashoffset = length;
// Trigger a layout so styles are calculated & the browser
// picks up the starting position before animating
path.getBoundingClientRect();
// Define the transition
path.style.transition = path.style.WebkitTransition = 'stroke-dashoffset ' + timeUnit + 's ease-in-out';
path.style.strokeDashoffset = '0';

polygon.style.transition = polygon.style.WebkitTransition = 'none';
polygon.style.opacity = '0';
polygon.style.transition = polygon.style.WebkitTransition = 'fill-opacity ' + timeUnit/2 + 's ease-in-out ' + timeUnit + 's';
setTimeout(() => {
polygon.style.opacity = '1';
}, 1000 * timeUnit);
}
}
105 changes: 105 additions & 0 deletions scripts/generate_dep.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,105 @@
import re, sys, textwrap
from pathlib import Path
from typing import Iterable

PROJECT_ROOT = Path(__file__).resolve().parents[1]
THEORIES_ROOT = PROJECT_ROOT / "theories"
ROOT_MODULE_NAME = "Mcltt"
COLORS = {
"Algorithmic": "darkturquoise",
"Completeness": "deeppink3",
"Core": "goldenrod",
"Entrypoint": "steelblue1",
"Syntactic": "darkorange",
"Semantic": "forestgreen",
"Soundness": "goldenrod1",
"Frontend": "darkslategray4",
"Extraction": "darkslategray3",
"others": "lightpink",
}

GRAPH_SET: set[str] = set()
RANKED_GRAPH_SET: set[str] = set()

def under_subgraph(name: str, body: str) -> str:
return f"""subgraph "{name}" {{ {body} }}"""

def subgraph_decl(*, name: str, label: str = "", tooltip: str = "", color: str, body: str = "") -> str:
GRAPH_SET.add(name)
return under_subgraph(name, f"""graph[color={color},fontcolor={color},label="{label}",tooltip="{tooltip}"]; node[fillcolor={color}]; {body}""")

def default_subgraph_decl(name: str, body: str = "") -> str:
return subgraph_decl(name=name, label=name, tooltip=f"{ROOT_MODULE_NAME}.{name}", color=COLORS[name], body=body)

def core_subgraph_decl(name: str, body: str = "") -> str:
return under_subgraph("Core", subgraph_decl(name=f"Core/{name}", label=name, tooltip=f"{ROOT_MODULE_NAME}.Core.{name}", color=COLORS[name], body=body))

DEPLINE_PATTERN = re.compile(r"(\S*\.vo).*:(.*)")
DEPSOURCE_PATTERN = re.compile(r"\S*\.vo")

def module_parts_of_path(path: str) -> tuple[str, ...]:
return Path(path).resolve().relative_to(THEORIES_ROOT).with_suffix("").parts

def module_name_of_module_parts(parts: Iterable[str]) -> str:
return f"""{ROOT_MODULE_NAME}.{".".join(parts)}"""

def module_name_of_path(path: str) -> str:
return module_name_of_module_parts(module_parts_of_path(path))

def node_of_path(path: str) -> str:
parts = module_parts_of_path(path)
color = next((COLORS[parts[i]] for i in range(len(parts)-1,-1,-1) if parts[i] in COLORS),COLORS["others"])
subgraph_names = ["/".join(parts[:partindex]) for partindex in range(1,len(parts))]
module_name = module_name_of_module_parts(parts)
node_label = parts[-1]

# Handle special case for two main theorems
# so that printed graph looks better
if module_name == "Mcltt.Core.Completeness" or module_name == "Mcltt.Core.Soundness":
result = under_subgraph(f"Core/{node_label}", f""""{module_name}"[label="{node_label}",tooltip="{module_name}",color={color},fillcolor=white];""")
elif module_name == "Mcltt.LibTactics":
result = f"""{{ graph[cluster=false,rank=min]; "{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}]; }}"""
else:
result = f""""{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}];"""

for subgraph_name in reversed(subgraph_names):
if subgraph_name in GRAPH_SET:
if subgraph_name in RANKED_GRAPH_SET:
result = under_subgraph(f"{subgraph_name}/rank", result)
result = under_subgraph(subgraph_name, result)
else:
GRAPH_SET.add(subgraph_name)
RANKED_GRAPH_SET.add(subgraph_name)
result = under_subgraph(f"{subgraph_name}/rank", f"graph[cluster=false,rank=same]; {result}")
result = under_subgraph(subgraph_name, f"""graph[cluster=true,label={parts[subgraph_names.index(subgraph_name)]},tooltip="{module_name_of_module_parts(subgraph_name.split("/"))}"]; {result}""")

return result

def data_of_depline(depline: str) -> str:
if result := DEPLINE_PATTERN.fullmatch(depline.strip()):
sink_module = module_name_of_path(result.group(1))
source_paths = result.group(2).split(" ")
source_modules = (module_name_of_path(source_path) for source_path in source_paths if DEPSOURCE_PATTERN.match(source_path))
edges = "\n".join(f""""{source_module}" -> "{sink_module}";""" for source_module in source_modules)
return f"""{edges}{node_of_path(result.group(1))}"""
else:
raise ValueError(f"Broken Dependency: \"{depline}\"")

def gen_graph() -> str:
newline = "\n"
return textwrap.dedent(f"""
digraph Mcltt {{
graph [center=true,class="depgraph",cluster=true,fontname="Open Sans",fontsize=28,label="Mcltt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""];
node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McLTT/\\N.html"];
{default_subgraph_decl("Algorithmic")}
{default_subgraph_decl("Core")}
{core_subgraph_decl("Completeness")}
{core_subgraph_decl("Semantic")}
{core_subgraph_decl("Soundness")}
{core_subgraph_decl("Syntactic")}
{default_subgraph_decl("Extraction")}
{default_subgraph_decl("Frontend")}
{textwrap.indent(newline.join(data_of_depline(depline) for depline in sys.stdin), " ").lstrip()}
}}""")

print(gen_graph())
17 changes: 17 additions & 0 deletions scripts/post_process_dep.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
from pathlib import Path
from xml.dom.minidom import parse
import io, sys

PROJECT_ROOT = Path(__file__).resolve().parents[1]
SVG = parse(sys.stdin)
SVG_ELEMENT = SVG.getElementsByTagName("svg")[0]
ENTIRE_GRAPH_ELEMENT = SVG_ELEMENT.getElementsByTagName("g")[0]
ENTIRE_GRAPH_ELEMENT.removeChild(ENTIRE_GRAPH_ELEMENT.getElementsByTagName("title")[0])
SVG_ELEMENT.setAttribute("onload", "makeEdgesInteractive(evt)")
for line in io.open(PROJECT_ROOT / "assets" / "extra" / "header.html"):
print(line, end='')
print('<link href="resources/depgraph.css" rel="stylesheet" type="text/css" />')
print('<script type="text/javascript" src="resources/depgraph.js"></script>')
SVG_ELEMENT.writexml(sys.stdout)
for line in io.open(PROJECT_ROOT / "assets" / "extra" / "footer.html"):
print(line, end='')
48 changes: 39 additions & 9 deletions theories/CoqMakefile.mk.local-late
Original file line number Diff line number Diff line change
Expand Up @@ -11,25 +11,55 @@ PARSERMESSAGEMERGEFILE := $(PARSERMESSAGEFILE:%.messages=%.messages.merge)
PARSERMESSAGEEXTRACTIONFILE := ../driver/extracted/ParserMessages.ml
COQPARSERORIGFILE := $(shell find ./ -name '*.vy')
COQPARSERFILE := $(COQPARSERORIGFILE:%.vy=%.v)
DEPGRAPHSCRIPT := ../scripts/generate_dep.py
DEPPOSTPROCESSSCRIPT := ../scripts/post_process_dep.py
DEPGRAPHDOT := dep.dot
DEPGRAPHDOC := dep.html
EXTRA_DIR := ../assets/extra
COQDOCFLAGS := \
--toc --toc-depth 2 --html --interpolate \
--index indexpage --no-lib-name --parse-comments \
--with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
export COQDOCFLAGS

# post-all:: $(COQPARSERFILE) $(PARSERMESSAGEEXTRACTIONFILE) check_parserMessages
# @echo "Separate Extraction main." | $(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile Entrypoint.v -l Entrypoint.v

$(COQPARSERFILE): %.v : %.vy
$(MENHIR) --coq "$?"
@echo "MENHIR $?"
@$(MENHIR) --coq "$?"

$(PARSERMESSAGEEXTRACTIONFILE): $(PARSERMESSAGEFILE) $(COQPARSERORIGFILE)
$(MENHIR) --coq "$(COQPARSERORIGFILE)" --compile-errors "$(PARSERMESSAGEFILE)" > "$(PARSERMESSAGEEXTRACTIONFILE)"
@echo "MENHIR $? PARSER MESSAGE"
@$(MENHIR) --coq "$(COQPARSERORIGFILE)" --compile-errors "$(PARSERMESSAGEFILE)" > "$(PARSERMESSAGEEXTRACTIONFILE)"

.PHONY: check_parserMessages
check_parserMessages:
$(MENHIR) --coq "$(COQPARSERORIGFILE)" --list-errors > "$(PARSERMESSAGETEMPFILE)"
$(MENHIR) --coq "$(COQPARSERORIGFILE)" --compare-errors "$(PARSERMESSAGETEMPFILE)" --compare-errors "$(PARSERMESSAGEFILE)"
rm "$(PARSERMESSAGETEMPFILE)"
@echo "MENHIR $? CHECK PARSER MESSAGE"
@$(MENHIR) --coq "$(COQPARSERORIGFILE)" --list-errors > "$(PARSERMESSAGETEMPFILE)"
@$(MENHIR) --coq "$(COQPARSERORIGFILE)" --compare-errors "$(PARSERMESSAGETEMPFILE)" --compare-errors "$(PARSERMESSAGEFILE)"
@rm "$(PARSERMESSAGETEMPFILE)"

.PHONY: update_parserMessages
update_parserMessages:
$(MENHIR) --coq "$(COQPARSERORIGFILE)" --list-errors > "$(PARSERMESSAGETEMPFILE)"
$(MENHIR) --coq "$(COQPARSERORIGFILE)" --merge-errors "$(PARSERMESSAGETEMPFILE)" --merge-errors "$(PARSERMESSAGEFILE)" > "$(PARSERMESSAGEMERGEFILE)"
rm "$(PARSERMESSAGETEMPFILE)"
mv "$(PARSERMESSAGEMERGEFILE)" "$(PARSERMESSAGEFILE)"
@echo "MENHIR $? UPDATE PARSER MESSAGE"
@$(MENHIR) --coq "$(COQPARSERORIGFILE)" --list-errors > "$(PARSERMESSAGETEMPFILE)"
@$(MENHIR) --coq "$(COQPARSERORIGFILE)" --merge-errors "$(PARSERMESSAGETEMPFILE)" --merge-errors "$(PARSERMESSAGEFILE)" > "$(PARSERMESSAGEMERGEFILE)"
@rm "$(PARSERMESSAGETEMPFILE)"
@mv "$(PARSERMESSAGEMERGEFILE)" "$(PARSERMESSAGEFILE)"

.PHONY: coqdoc
coqdoc: html
cp -R $(EXTRA_DIR)/resources html

$(DEPGRAPHDOT): $(VFILES) $(DEPGRAPHSCRIPT)
@coqdep $(VFILES) -f _CoqProject | python3 "$(DEPGRAPHSCRIPT)" | tred > "$@"

$(DEPGRAPHDOC): $(DEPGRAPHDOT) $(DEPPOSTPROCESSSCRIPT)
@dot -T svg "$(DEPGRAPHDOT)" | python3 "$(DEPPOSTPROCESSSCRIPT)" > "$(DEPGRAPHDOC)"

.PHONY: depgraphdoc
depgraphdoc: $(DEPGRAPHDOC)

clean::
@rm $(DEPGRAPHDOT) $(DEPGRAPHDOC)
2 changes: 1 addition & 1 deletion theories/Core/Syntactic/CoreInversions.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From Coq Require Import Setoid.
From Mcltt Require Import Base LibTactics CtxSub.
From Mcltt Require Import Base LibTactics.
From Mcltt.Core Require Export SystemOpt.
Import Syntax_Notations.

Expand Down
Loading

0 comments on commit 522b9c6

Please sign in to comment.