Skip to content

Commit

Permalink
website: rewritten procs documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
Philipp15b committed Jan 2, 2025
1 parent f51af62 commit c56a577
Show file tree
Hide file tree
Showing 7 changed files with 418 additions and 53 deletions.
4 changes: 2 additions & 2 deletions website/docs/heyvl/domains.md
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@ proc ohfive_3() -> ()
{}
```

**Do not forget the _empty_ block of statements `{}` at the end!**
If you omit it, Caesar will not attempt to verify the procedure and thus will not check the specification.
Do not forget the _empty_ block of statements `{}` at the end.
If you omit it, [Caesar will not attempt to verify the procedure](./procs.md#procs-without-body) and thus will not check the specification.

## Pure Functions

Expand Down
312 changes: 267 additions & 45 deletions website/docs/heyvl/procs.md

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions website/docs/heyvl/statements.md
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,8 @@ x, y = two_numbers()

If the right-hand side of the assignment is a (pure) expression, then the verification condition semantics amounts to a substitution of the left-hand side by the right-hand side.

If the right-hand side is a call to a procedure, then the assignment is translated to a combination of `assert`, `havoc`, and `compare` statements.
See the [reference on procedures](./procs.md) for more information.
The right-hand side of the assignment can be a procedure call.
See the [reference on procedure calls](./procs.md#calling-procedures) for more information.

If the procedure does not have any return values, the call may be written without the equals sign and the left-hand side, i.e. simply `fn(arg1, arg2)`.

Expand Down
16 changes: 14 additions & 2 deletions website/docusaurus.config.js
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@
// Note: type annotations allow type checking and IDEs autocompletion

import {themes as prismThemes} from 'prism-react-renderer';
import remarkMath from 'remark-math';
import rehypeKatex from 'rehype-katex';

/** @type {import('@docusaurus/types').Config} */
const config = {
Expand Down Expand Up @@ -44,10 +46,10 @@ const config = {
({
docs: {
sidebarPath: require.resolve('./sidebars.js'),
// Please change this to your repo.
// Remove this to remove the "edit this page" links.
editUrl:
'https://github.com/moves-rwth/caesar/tree/main/website/',
remarkPlugins: [remarkMath],
rehypePlugins: [rehypeKatex],
},
blog: {
blogSidebarCount: 20,
Expand All @@ -66,6 +68,16 @@ const config = {
],
],

stylesheets: [
{
href: 'https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css',
type: 'text/css',
integrity:
'sha384-odtC+0UGzzFL/6PNoE8rX/SPcQDXBJ+uRepguP4QkPCm2LBxH3FA3y+fKSiJ+AmM',
crossorigin: 'anonymous',
},
],

themeConfig:
/** @type {import('@docusaurus/preset-classic').ThemeConfig} */
({
Expand Down
4 changes: 3 additions & 1 deletion website/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,9 @@
"clsx": "^1.2.1",
"prism-react-renderer": "^2.1.0",
"react": "^18.2.0",
"react-dom": "^18.2.0"
"react-dom": "^18.2.0",
"rehype-katex": "7",
"remark-math": "6"
},
"devDependencies": {
"@docusaurus/module-type-aliases": "^3.6.0"
Expand Down
4 changes: 4 additions & 0 deletions website/src/css/custom.css
Original file line number Diff line number Diff line change
Expand Up @@ -59,3 +59,7 @@ a.button {
display: inherit;
}
}

/* by default, katex equations are bigger than the surrounding text. we want our
math to nicely be contained in the surrounding text. */
.katex { font-size: 1em !important; }
127 changes: 126 additions & 1 deletion website/yarn.lock
Original file line number Diff line number Diff line change
Expand Up @@ -2912,6 +2912,11 @@
resolved "https://registry.yarnpkg.com/@types/json-schema/-/json-schema-7.0.13.tgz#02c24f4363176d2d18fc8b70b9f3c54aba178a85"
integrity sha512-RbSSoHliUbnXj3ny0CNFOoxrIDV6SUGyStHsvDqosw6CkdPV8TtWGlfecuK4ToyMEAql6pzNxgCFKanovUzlgQ==

"@types/katex@^0.16.0":
version "0.16.7"
resolved "https://registry.yarnpkg.com/@types/katex/-/katex-0.16.7.tgz#03ab680ab4fa4fbc6cb46ecf987ecad5d8019868"
integrity sha512-HMwFiRujE5PjrgwHQ25+bsLJgowjGjm5Z8FVSf0N6PwgJrwxH0QxzHYDcKsTfV3wva0vzrpqMTJS2jXPr5BMEQ==

"@types/mdast@^4.0.0", "@types/mdast@^4.0.2":
version "4.0.4"
resolved "https://registry.yarnpkg.com/@types/mdast/-/mdast-4.0.4.tgz#7ccf72edd2f1aa7dd3437e180c64373585804dd6"
Expand Down Expand Up @@ -5647,6 +5652,37 @@ has@^1.0.3:
resolved "https://registry.yarnpkg.com/has/-/has-1.0.4.tgz#2eb2860e000011dae4f1406a86fe80e530fb2ec6"
integrity sha512-qdSAmqLF6209RFj4VVItywPMbm3vWylknmB3nvNiUIs72xAimcM8nVYxYr7ncvZq5qzk9MKIZR8ijqD/1QuYjQ==

hast-util-from-dom@^5.0.0:
version "5.0.1"
resolved "https://registry.yarnpkg.com/hast-util-from-dom/-/hast-util-from-dom-5.0.1.tgz#c3c92fbd8d4e1c1625edeb3a773952b9e4ad64a8"
integrity sha512-N+LqofjR2zuzTjCPzyDUdSshy4Ma6li7p/c3pA78uTwzFgENbgbUrm2ugwsOdcjI1muO+o6Dgzp9p8WHtn/39Q==
dependencies:
"@types/hast" "^3.0.0"
hastscript "^9.0.0"
web-namespaces "^2.0.0"

hast-util-from-html-isomorphic@^2.0.0:
version "2.0.0"
resolved "https://registry.yarnpkg.com/hast-util-from-html-isomorphic/-/hast-util-from-html-isomorphic-2.0.0.tgz#b31baee386a899a2472326a3c5692f29f86d1d3c"
integrity sha512-zJfpXq44yff2hmE0XmwEOzdWin5xwH+QIhMLOScpX91e/NSGPsAzNCvLQDIEPyO2TXi+lBmU6hjLIhV8MwP2kw==
dependencies:
"@types/hast" "^3.0.0"
hast-util-from-dom "^5.0.0"
hast-util-from-html "^2.0.0"
unist-util-remove-position "^5.0.0"

hast-util-from-html@^2.0.0:
version "2.0.3"
resolved "https://registry.yarnpkg.com/hast-util-from-html/-/hast-util-from-html-2.0.3.tgz#485c74785358beb80c4ba6346299311ac4c49c82"
integrity sha512-CUSRHXyKjzHov8yKsQjGOElXy/3EKpyX56ELnkHH34vDVw1N1XSQ1ZcAvTyAPtGqLTuKP/uxM+aLkSPqF/EtMw==
dependencies:
"@types/hast" "^3.0.0"
devlop "^1.1.0"
hast-util-from-parse5 "^8.0.0"
parse5 "^7.0.0"
vfile "^6.0.0"
vfile-message "^4.0.0"

hast-util-from-parse5@^8.0.0:
version "8.0.2"
resolved "https://registry.yarnpkg.com/hast-util-from-parse5/-/hast-util-from-parse5-8.0.2.tgz#29b42758ba96535fd6021f0f533c000886c0f00f"
Expand All @@ -5661,6 +5697,13 @@ hast-util-from-parse5@^8.0.0:
vfile-location "^5.0.0"
web-namespaces "^2.0.0"

hast-util-is-element@^3.0.0:
version "3.0.0"
resolved "https://registry.yarnpkg.com/hast-util-is-element/-/hast-util-is-element-3.0.0.tgz#6e31a6532c217e5b533848c7e52c9d9369ca0932"
integrity sha512-Val9mnv2IWpLbNPqc/pUem+a7Ipj2aHacCwgNfTiK0vJKl0LF+4Ba4+v1oPHFpf3bLYmreq0/l3Gud9S5OH42g==
dependencies:
"@types/hast" "^3.0.0"

hast-util-parse-selector@^4.0.0:
version "4.0.0"
resolved "https://registry.yarnpkg.com/hast-util-parse-selector/-/hast-util-parse-selector-4.0.0.tgz#352879fa86e25616036037dd8931fb5f34cb4a27"
Expand Down Expand Up @@ -5743,6 +5786,16 @@ hast-util-to-parse5@^8.0.0:
web-namespaces "^2.0.0"
zwitch "^2.0.0"

hast-util-to-text@^4.0.0:
version "4.0.2"
resolved "https://registry.yarnpkg.com/hast-util-to-text/-/hast-util-to-text-4.0.2.tgz#57b676931e71bf9cb852453678495b3080bfae3e"
integrity sha512-KK6y/BN8lbaq654j7JgBydev7wuNMcID54lkRav1P0CaE1e47P72AWWPiGKXTJU271ooYzcvTAn/Zt0REnvc7A==
dependencies:
"@types/hast" "^3.0.0"
"@types/unist" "^3.0.0"
hast-util-is-element "^3.0.0"
unist-util-find-after "^5.0.0"

hast-util-whitespace@^3.0.0:
version "3.0.0"
resolved "https://registry.yarnpkg.com/hast-util-whitespace/-/hast-util-whitespace-3.0.0.tgz#7778ed9d3c92dd9e8c5c8f648a49c21fc51cb621"
Expand Down Expand Up @@ -6374,6 +6427,13 @@ jsonfile@^6.0.1:
optionalDependencies:
graceful-fs "^4.1.6"

katex@^0.16.0:
version "0.16.19"
resolved "https://registry.yarnpkg.com/katex/-/katex-0.16.19.tgz#698e026188876f9c8c93d3ecb27b212aaa056d0a"
integrity sha512-3IA6DYVhxhBabjSLTNO9S4+OliA3Qvb8pBQXMfC4WxXJgLwZgnfDl0BmB4z6nBMdznBsZ+CGM8DrGZ5hcguDZg==
dependencies:
commander "^8.3.0"

katex@^0.16.9:
version "0.16.18"
resolved "https://registry.yarnpkg.com/katex/-/katex-0.16.18.tgz#20781284288bc52805c519e48ac756163ad4b1f3"
Expand Down Expand Up @@ -6712,6 +6772,19 @@ mdast-util-gfm@^3.0.0:
mdast-util-gfm-task-list-item "^2.0.0"
mdast-util-to-markdown "^2.0.0"

mdast-util-math@^3.0.0:
version "3.0.0"
resolved "https://registry.yarnpkg.com/mdast-util-math/-/mdast-util-math-3.0.0.tgz#8d79dd3baf8ab8ac781f62b8853768190b9a00b0"
integrity sha512-Tl9GBNeG/AhJnQM221bJR2HPvLOSnLE/T9cJI9tlc6zwQk2nPk/4f0cHkOdEixQPC/j8UtKDdITswvLAy1OZ1w==
dependencies:
"@types/hast" "^3.0.0"
"@types/mdast" "^4.0.0"
devlop "^1.0.0"
longest-streak "^3.0.0"
mdast-util-from-markdown "^2.0.0"
mdast-util-to-markdown "^2.1.0"
unist-util-remove-position "^5.0.0"

mdast-util-mdx-expression@^2.0.0:
version "2.0.1"
resolved "https://registry.yarnpkg.com/mdast-util-mdx-expression/-/mdast-util-mdx-expression-2.0.1.tgz#43f0abac9adc756e2086f63822a38c8d3c3a5096"
Expand Down Expand Up @@ -6788,7 +6861,7 @@ mdast-util-to-hast@^13.0.0:
unist-util-visit "^5.0.0"
vfile "^6.0.0"

mdast-util-to-markdown@^2.0.0:
mdast-util-to-markdown@^2.0.0, mdast-util-to-markdown@^2.1.0:
version "2.1.2"
resolved "https://registry.yarnpkg.com/mdast-util-to-markdown/-/mdast-util-to-markdown-2.1.2.tgz#f910ffe60897f04bb4b7e7ee434486f76288361b"
integrity sha512-xj68wMTvGXVOKonmog6LwyJKrYXZPvlwabaryTjLh9LuvovB/KAH+kvi8Gjj+7rJjsFi23nkUxRQv1KqSroMqA==
Expand Down Expand Up @@ -7002,6 +7075,19 @@ micromark-extension-gfm@^3.0.0:
micromark-util-combine-extensions "^2.0.0"
micromark-util-types "^2.0.0"

micromark-extension-math@^3.0.0:
version "3.1.0"
resolved "https://registry.yarnpkg.com/micromark-extension-math/-/micromark-extension-math-3.1.0.tgz#c42ee3b1dd5a9a03584e83dd8f08e3de510212c1"
integrity sha512-lvEqd+fHjATVs+2v/8kg9i5Q0AP2k85H0WUOwpIVvUML8BapsMvh1XAogmQjOCsLpoKRCVQqEkQBB3NhVBcsOg==
dependencies:
"@types/katex" "^0.16.0"
devlop "^1.0.0"
katex "^0.16.0"
micromark-factory-space "^2.0.0"
micromark-util-character "^2.0.0"
micromark-util-symbol "^2.0.0"
micromark-util-types "^2.0.0"

micromark-extension-mdx-expression@^3.0.0:
version "3.0.0"
resolved "https://registry.yarnpkg.com/micromark-extension-mdx-expression/-/micromark-extension-mdx-expression-3.0.0.tgz#1407b9ce69916cf5e03a196ad9586889df25302a"
Expand Down Expand Up @@ -8852,6 +8938,19 @@ regjsparser@^0.9.1:
dependencies:
jsesc "~0.5.0"

rehype-katex@7:
version "7.0.1"
resolved "https://registry.yarnpkg.com/rehype-katex/-/rehype-katex-7.0.1.tgz#832e6d7af2744a228981d1b0fe89483a9e7c93a1"
integrity sha512-OiM2wrZ/wuhKkigASodFoo8wimG3H12LWQaH8qSPVJn9apWKFSH3YOCtbKpBorTVw/eI7cuT21XBbvwEswbIOA==
dependencies:
"@types/hast" "^3.0.0"
"@types/katex" "^0.16.0"
hast-util-from-html-isomorphic "^2.0.0"
hast-util-to-text "^4.0.0"
katex "^0.16.0"
unist-util-visit-parents "^6.0.0"
vfile "^6.0.0"

rehype-raw@^7.0.0:
version "7.0.0"
resolved "https://registry.yarnpkg.com/rehype-raw/-/rehype-raw-7.0.0.tgz#59d7348fd5dbef3807bbaa1d443efd2dd85ecee4"
Expand Down Expand Up @@ -8918,6 +9017,16 @@ remark-gfm@^4.0.0:
remark-stringify "^11.0.0"
unified "^11.0.0"

remark-math@6:
version "6.0.0"
resolved "https://registry.yarnpkg.com/remark-math/-/remark-math-6.0.0.tgz#0acdf74675f1c195fea6efffa78582f7ed7fc0d7"
integrity sha512-MMqgnP74Igy+S3WwnhQ7kqGlEerTETXMvJhrUzDikVZ2/uogJCb+WHUg97hK9/jcfc0dkD73s3LN8zU49cTEtA==
dependencies:
"@types/mdast" "^4.0.0"
mdast-util-math "^3.0.0"
micromark-extension-math "^3.0.0"
unified "^11.0.0"

remark-mdx@^3.0.0:
version "3.1.0"
resolved "https://registry.yarnpkg.com/remark-mdx/-/remark-mdx-3.1.0.tgz#f979be729ecb35318fa48e2135c1169607a78343"
Expand Down Expand Up @@ -9816,6 +9925,14 @@ unique-string@^3.0.0:
dependencies:
crypto-random-string "^4.0.0"

unist-util-find-after@^5.0.0:
version "5.0.0"
resolved "https://registry.yarnpkg.com/unist-util-find-after/-/unist-util-find-after-5.0.0.tgz#3fccc1b086b56f34c8b798e1ff90b5c54468e896"
integrity sha512-amQa0Ep2m6hE2g72AugUItjbuM8X8cGQnFoHk0pGfrFeT9GZhzN5SW8nRsiGKK7Aif4CrACPENkA6P/Lw6fHGQ==
dependencies:
"@types/unist" "^3.0.0"
unist-util-is "^6.0.0"

unist-util-is@^6.0.0:
version "6.0.0"
resolved "https://registry.yarnpkg.com/unist-util-is/-/unist-util-is-6.0.0.tgz#b775956486aff107a9ded971d996c173374be424"
Expand All @@ -9837,6 +9954,14 @@ unist-util-position@^5.0.0:
dependencies:
"@types/unist" "^3.0.0"

unist-util-remove-position@^5.0.0:
version "5.0.0"
resolved "https://registry.yarnpkg.com/unist-util-remove-position/-/unist-util-remove-position-5.0.0.tgz#fea68a25658409c9460408bc6b4991b965b52163"
integrity sha512-Hp5Kh3wLxv0PHj9m2yZhhLt58KzPtEYKQQ4yxfYFEO7EvHwzyDYnduhHnY1mDxoqr7VUwVuHXk9RXKIiYS1N8Q==
dependencies:
"@types/unist" "^3.0.0"
unist-util-visit "^5.0.0"

unist-util-stringify-position@^4.0.0:
version "4.0.0"
resolved "https://registry.yarnpkg.com/unist-util-stringify-position/-/unist-util-stringify-position-4.0.0.tgz#449c6e21a880e0855bf5aabadeb3a740314abac2"
Expand Down

0 comments on commit c56a577

Please sign in to comment.