Skip to content

Inlined documentation #783

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 23 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
9a06377
Maintain documentation comments and construct basic HTML files from t…
strub Sep 11, 2023
34c1d9c
Additional styling for HTML files.
MM45 Jun 17, 2024
11bb6f8
First progress for markdown.
strub Jul 12, 2024
9bfb08b
Merge branch 'main' into inlined-doc
strub Aug 20, 2024
e146a6d
Fix styling with markdown generation and add additional logic for get…
MM45 Aug 20, 2024
1dcdd91
First complete attempt at linking items (locally, not from stdlib).
MM45 Aug 21, 2024
a302c28
Add support for linking to nested abstract theories.
MM45 Aug 22, 2024
e7bda8d
Default documentation when missing.
MM45 Aug 22, 2024
3789848
Add separate command for documenation generation and add option for s…
MM45 Sep 6, 2024
e2523d3
Merge remote-tracking branch 'origin/main' into inlined-doc
strub May 26, 2025
a9b40e9
deps
strub May 27, 2025
f37090d
Surely this works better?
MM45 May 28, 2025
9c42290
Change syntax for documentation comments, preventing conflicts
MM45 May 29, 2025
cba4216
Markdown in INSTALL.md, change styling, and docgen tutorial/test.
MM45 May 30, 2025
ab09afb
Delete outdated docgen test.
MM45 May 30, 2025
77b8c7b
Delete file with outdated information.
MM45 May 30, 2025
546c1d3
Consistency in styles
MM45 May 30, 2025
a70d42d
WIP in lexer
strub Jun 2, 2025
1413188
Remove warnings, specific exception handling, and update example
MM45 Jun 2, 2025
2db1417
Address feedback and fix bug that generated docs for cloned theories
MM45 Jun 17, 2025
ff21f5a
Delete empty directory and rename
MM45 Jun 17, 2025
ec0eb22
Why check yourself when you can also let CI check?
MM45 Jun 17, 2025
279abe9
Don't let docgen be stopped by eco file nor check any proofs
MM45 Jun 25, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions INSTALL.md
Original file line number Diff line number Diff line change
Expand Up @@ -522,6 +522,9 @@ proceed to [install EasyCrypt from Source](#installing-easycrypt-from-source).
- [OCaml ini-files](https://opam.ocaml.org/packages/ocaml-inifiles/) (version >= 1.2)
Additional resources:
- http://archive.ubuntu.com/ubuntu/pool/universe/o/ocaml-inifiles
- [OCaml Markdown](https://github.com/gildor478/ocaml-markdown)
Additional resources:
- https://opam.ocaml.org/packages/markdown
- [Python3](https://www.python.org/downloads)
You also need to install the following libraries:
- [Python3 YAML](https://pyyaml.org/wiki/PyYAMLDocumentation)
Expand Down
Empty file added assets/.gitignore
Empty file.
228 changes: 228 additions & 0 deletions assets/styles/styles.css
Original file line number Diff line number Diff line change
@@ -0,0 +1,228 @@
/* General Styling */
/* Body */
body {
font-family: "-apple-system", "BlinkMacSystemFont", "Roboto", "Arial", sans-serif;
line-height: 1.2;
font-size: 16px;
margin: 0;
padding: 0;
color: #333;
background-color: #f9f9f9;
}

/* Code blocks */
pre {
font-family: "Fira Code", "Consolas", monospace;
font-size: 1rem;
padding: 5px;
border-radius: 1px;
color: #2d2d2d;
background-color: #ecf0f1;
}

/* Inline code */
code {
font-family: "Fira Code", "Consolas", monospace;
font-size: 1rem;
color: #d6336c;
}

/* Headings */
h1, h2, h3, h4, h5, h6 {
font-family: "Roboto", "Arial", sans-serif;
font-weight: 600;
color: #1a1a1a;
margin-bottom: 0.5em;
}

h1 {
font-size: 2.25rem;
}
h2 {
font-size: 2rem;
}
h3 {
font-size: 1.75rem;
}
h4 {
font-size: 1.5rem;
}
h5 {
font-size: 1.25rem;
}
h6 {
font-size: 1rem;
}

/* Links */
a {
font-family: "Roboto", "Arial", sans-serif;
color: #007bff;
text-decoration: none;
}

a:hover {
color: #0056b3;
text-decoration: underline;
}

.serif-text {
font-family: "Times New Roman", "Times", serif;
font-size: 1rem;
color: #333;
}

/* Specific styling */

/* Sidebar */
.sidebar {
width: 200px;
background-color: #2c3e50;
color: #ecf0f1;
position: fixed;
height: 100%;
overflow: auto;
}

.sidebar-title {
padding: 20px;
color: #ecf0f1;
background-color: #34495e;
margin-bottom: 20px;
}

.sidebar-title h2 {
font-size: 1.5em;
margin-bottom: 5px;
color: #ecf0f1;
}

.sidebar-title .sidebar-title-theory {
font-size: 1.2em;
color: #3498db;
}

.sidebar-title-theory {
word-wrap: break-word;
overflow-wrap: break-word;
white-space: normal;
}

.sidebar-elems {
padding: 20px;
}

.sidebar-section-list {
list-style: none;
padding: 0;
}

.sidebar-section-list li {
margin: 15px 0;
}

.sidebar-section-list li a {
color: #ecf0f1;
font-weight: bold;
}

/* Main content */
main {
margin-left: 220px;
padding: 20px;
max-width: 960px;
}

.page-heading-container {
border-bottom: 2px solid #ddd;
padding-bottom: 5px;
margin-bottom: 20px;
}

.page-heading-container .page-heading {
margin-block-end: 5px;
}

.page-heading-container .page-subheading {
margin-block-start: 0px;
margin-block-end: 5px;
font-size: 1.2em;
}

/* Sections */
.item-section {
margin-bottom: 40px;
}

.section-heading {
color: #34495e;
border-bottom: 2px solid #ddd;
padding-bottom: 10px;
margin-bottom: 20px;
}

/* Item lists */
.item-list {
list-style: none;
padding: 0;
}

.item-entry {
display: flex;
flex-direction: column;
margin-bottom: 20px;
}

.item-name-desc-container {
display: flex;
align-items: flex-start;
}

.item-name {
width: 200px;
font-weight: bold;
color: #2980b9;
white-space: normal;
overflow-wrap: break-word;
}

.item-basic-desc {
flex: 1;
margin-left: 10px;
}

.item-basic-desc p {
margin-top: 0px;
}

.item-details {
margin-left: 210px;
}

.item-details summary {
cursor: pointer;
color: #3498db;
font-weight: bold;
}

.item-details summary:hover {
text-decoration: underline;
}

.item-details-par {
margin-top: 10px;
}

/* Source code */
pre.source {
border: 2px solid #bdc3c7;
padding: 10px;
border-radius: 5px;
overflow-x: auto;
white-space: pre-wrap;
}

/* Introduction section */
.intro-section {
margin-bottom: 40px;
}
6 changes: 5 additions & 1 deletion dune
Original file line number Diff line number Diff line change
@@ -1,9 +1,13 @@
(dirs src theories examples scripts)
(dirs src theories examples scripts assets)

(install
(section (site (easycrypt commands)))
(files (scripts/testing/runtest as runtest)))

(install
(section (site (easycrypt doc)))
(files (assets/styles/styles.css as styles.css)))

(install
(section (bin))
(files (scripts/testing/bin-ec-runtest as ec-runtest)))
3 changes: 2 additions & 1 deletion dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@

(package
(name easycrypt)
(sites (lib theories) (libexec commands))
(sites (lib theories) (libexec commands) (lib doc))
(depends
(ocaml (>= 4.08.0))
(batteries (>= 3))
Expand All @@ -19,6 +19,7 @@
dune
dune-build-info
dune-site
markdown
(ocaml-inifiles (>= 1.2))
(pcre (>= 7))
(why3 (and (>= 1.8.0) (< 1.9)))
Expand Down
1 change: 1 addition & 0 deletions easycrypt.opam
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ depends: [
"dune" {>= "3.13"}
"dune-build-info"
"dune-site"
"markdown"
"ocaml-inifiles" {>= "1.2"}
"pcre" {>= "7"}
"why3" {>= "1.8.0" & < "1.9"}
Expand Down
Loading