diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index d7c5be3105..cb4e5575d4 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -6,6 +6,12 @@ - [Quickstart](./quickstart.md) - [Theorem Proving in Lean](./tpil.md) - [Examples](./examples.md) + - [Palindromes](examples/palindromes.lean.md) + - [Binary Search Trees](examples/bintree.lean.md) + - [A Certified Type Checker](examples/tc.lean.md) + - [The Well-Typed Interpreter](examples/interp.lean.md) + - [Dependent de Bruijn Indices](examples/deBruijn.lean.md) + - [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.md) # Language Manual diff --git a/doc/alectryon.css b/doc/alectryon.css new file mode 100644 index 0000000000..fc4f05c0e8 --- /dev/null +++ b/doc/alectryon.css @@ -0,0 +1,772 @@ +@charset "UTF-8"; +/* +Copyright © 2019 Clément Pit-Claudel + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. +*/ + +/*******************************/ +/* CSS reset for .alectryon-io */ +/*******************************/ + +.alectryon-io blockquote { + line-height: inherit; +} + +.alectryon-io blockquote:after { + display: none; +} + +.alectryon-io label { + display: inline; + font-size: inherit; + margin: 0; +} + +.alectryon-io a { + text-decoration: none !important; + font-style: oblique !important; + color: unset; +} + +/* Undo and
, added to improve RSS rendering. */ + +.alectryon-io small.alectryon-output, +.alectryon-io small.alectryon-type-info { + font-size: inherit; +} + +.alectryon-io blockquote.alectryon-goal, +.alectryon-io blockquote.alectryon-message { + font-weight: normal; + font-size: inherit; +} + +/***************/ +/* Main styles */ +/***************/ + +.alectryon-coqdoc .doc .code, +.alectryon-coqdoc .doc .comment, +.alectryon-coqdoc .doc .inlinecode, +.alectryon-mref, +.alectryon-block, .alectryon-io, +.alectryon-toggle-label, .alectryon-banner { + font-family: 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab', 'Iosevka', 'Fira Code', monospace; + font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */; + line-height: initial; +} + +.alectryon-io, .alectryon-block, .alectryon-toggle-label, .alectryon-banner { + overflow: visible; + overflow-wrap: break-word; + position: relative; + white-space: pre-wrap; +} + +/* +CoqIDE doesn't turn off the unicode bidirectional algorithm (and PG simply +respects the user's `bidi-display-reordering` setting), so don't turn it off +here either. But beware unexpected results like `Definition test_אב := 0.` + +.alectryon-io span { + direction: ltr; + unicode-bidi: bidi-override; +} + +In any case, make an exception for comments: + +.highlight .c { + direction: embed; + unicode-bidi: initial; +} +*/ + +.alectryon-mref, +.alectryon-mref-marker { + align-self: center; + box-sizing: border-box; + display: inline-block; + font-size: 80%; + font-weight: bold; + line-height: 1; + box-shadow: 0 0 0 1pt black; + padding: 1pt 0.3em; + text-decoration: none; +} + +.alectryon-block .alectryon-mref-marker, +.alectryon-io .alectryon-mref-marker { + user-select: none; + margin: -0.25em 0 -0.25em 0.5em; +} + +.alectryon-inline .alectryon-mref-marker { + margin: -0.25em 0.15em -0.25em 0.625em; /* 625 = 0.5em / 80% */ +} + +.alectryon-mref { + color: inherit; + margin: -0.5em 0.25em; +} + +.alectryon-goal:target .goal-separator .alectryon-mref-marker, +:target > .alectryon-mref-marker { + animation: blink 0.2s step-start 0s 3 normal none; + background-color: #fcaf3e; + position: relative; +} + +@keyframes blink { + 50% { + box-shadow: 0 0 0 3pt #fcaf3e, 0 0 0 4pt black; + z-index: 10; + } +} + +.alectryon-toggle, +.alectryon-io .alectryon-extra-goal-toggle { + display: none; +} + +.alectryon-bubble, +.alectryon-io label, +.alectryon-toggle-label { + cursor: pointer; +} + +.alectryon-toggle-label { + display: block; + font-size: 0.8em; +} + +.alectryon-io .alectryon-input { + padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */ +} + +.alectryon-io .alectryon-token { + white-space: pre-wrap; + display: inline; +} + +.alectryon-io .alectryon-sentence.alectryon-target .alectryon-input { + /* FIXME if keywords were ‘bolder’ we wouldn't need !important */ + font-weight: bold !important; /* Use !important to avoid a * selector */ +} + +.alectryon-bubble:before, +.alectryon-toggle-label:before, +.alectryon-io label.alectryon-input:after, +.alectryon-io .alectryon-goal > label:before { + border: 1px solid #babdb6; + border-radius: 1em; + box-sizing: border-box; + content: ''; + display: inline-block; + font-weight: bold; + height: 0.25em; + margin-bottom: 0.15em; + vertical-align: middle; + width: 0.75em; +} + +.alectryon-toggle-label:before, +.alectryon-io .alectryon-goal > label:before { + margin-right: 0.25em; +} + +.alectryon-io .alectryon-goal > label:before { + margin-top: 0.125em; +} + +.alectryon-io label.alectryon-input { + padding-right: 1em; /* Prevent line wraps before the checkbox bubble */ +} + +.alectryon-io label.alectryon-input:after { + margin-left: 0.25em; + margin-right: -1em; /* Compensate for the anti-wrapping space */ +} + +.alectryon-failed { + /* Underlines are broken in Chrome (they reset at each element boundary)… */ + /* text-decoration: red wavy underline; */ + /* … but it isn't too noticeable with dots */ + text-decoration: red dotted underline; + text-decoration-skip-ink: none; + /* Chrome prints background images in low resolution, yielding a blurry underline */ + /* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */ +} + +/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence + doesn't trigger its :hover state (otherwise, on mobile, tapping a sentence to + hide its output causes it to remain visible (its :hover state gets triggered. + We only do it for the default style though, since other styles don't put the + output over the main text, so showing too much is not an issue. */ +@media (any-hover: hover) { + .alectryon-bubble:hover:before, + .alectryon-toggle-label:hover:before, + .alectryon-io label.alectryon-input:hover:after { + background: #eeeeec; + } + + .alectryon-io label.alectryon-input:hover { + text-decoration: underline dotted #babdb6; + text-shadow: 0 0 1px rgb(46, 52, 54, 0.3); /* #2e3436 + opacity */ + } + + .alectryon-io .alectryon-sentence:hover .alectryon-output, + .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper, + .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper { + z-index: 2; /* Place hovered goals above .alectryon-sentence.alectryon-target ones */ + } +} + +.alectryon-toggle:checked + .alectryon-toggle-label:before, +.alectryon-io .alectryon-sentence > .alectryon-toggle:checked + label.alectryon-input:after, +.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal > label:before { + background-color: #babdb6; + border-color: #babdb6; +} + +/* Disable clicks on sentences when the document-wide toggle is set. */ +.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input { + cursor: unset; + pointer-events: none; +} + +/* Hide individual checkboxes when the document-wide toggle is set. */ +.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input:after { + display: none; +} + +/* .alectryon-output is displayed by toggles, :hover, and .alectryon-target rules */ +.alectryon-io .alectryon-output { + box-sizing: border-box; + display: none; + left: 0; + right: 0; + position: absolute; + padding: 0.25em 0; + overflow: visible; /* Let box-shadows overflow */ + z-index: 1; /* Default to an index lower than that used by :hover */ +} + +.alectryon-io .alectryon-type-info-wrapper { + position: absolute; + display: inline-block; +} + +.alectryon-io .alectryon-type-info-wrapper.full-width { + left: 0; + min-width: 100%; + max-width: 100%; +} + +.alectryon-io .alectryon-type-info .goal-separator { + height: unset; + margin-top: 0em; +} + +.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info { + box-sizing: border-box; + bottom: 100%; + position: absolute; + padding: 0.25em 0; + visibility: hidden; + overflow: visible; /* Let box-shadows overflow */ + z-index: 1; /* Default to an index lower than that used by :hover */ + white-space: pre !important; +} + +.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info .alectryon-goal.alectryon-docstring { + white-space: pre-wrap !important; +} + +@media (any-hover: hover) { /* See note above about this @media query */ + .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) { + display: block; + } + + .alectryon-io.output-hidden .alectryon-sentence:hover .alectryon-output:not(:hover) { + display: none !important; + } + + .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info, + .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info { + visibility: hidden !important; + } + + .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info, + .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info { + visibility: visible; + } +} + +.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output { + display: block; +} + +/* Indicate active (hovered or targeted) goals with a shadow. */ +.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages, +.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-messages, +.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals, +.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-goals { + box-shadow: 0 0 3px gray; +} + +.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-hyps { + display: none; +} + +.alectryon-io .alectryon-extra-goals .alectryon-extra-goal-toggle:not(:checked) + .alectryon-goal label.goal-separator hr { + /* Dashes indicate that the hypotheses are hidden */ + border-top-style: dashed; +} + + +/* Show just a small preview of the other goals; this is undone by the + "extra-goal" toggle and by :hover and .alectryon-target in windowed mode. */ +.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-conclusion { + max-height: 5.2em; + overflow-y: auto; + /* Combining ‘overflow-y: auto’ with ‘display: inline-block’ causes extra space + to be added below the box. ‘vertical-align: middle’ gets rid of it. */ + vertical-align: middle; +} + +.alectryon-io .alectryon-goals, +.alectryon-io .alectryon-messages { + background: #eeeeec; + border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */ + display: block; + padding: 0.25em; +} + +.alectryon-message::before { + content: ''; + float: right; + /* etc/svg/square-bubble-xl.svg */ + background: url("data:image/svg+xml,%3Csvg width='14' height='14' viewBox='0 0 3.704 3.704' xmlns='http://www.w3.org/2000/svg'%3E%3Cg fill-rule='evenodd' stroke='%23000' stroke-width='.264'%3E%3Cpath d='M.794.934h2.115M.794 1.463h1.455M.794 1.992h1.852'/%3E%3C/g%3E%3Cpath d='M.132.14v2.646h.794v.661l.926-.661h1.72V.14z' fill='none' stroke='%23000' stroke-width='.265'/%3E%3C/svg%3E") top right no-repeat; + height: 14px; + width: 14px; +} + +.alectryon-toggle:checked + label + .alectryon-container { + width: unset; +} + +/* Show goals when a toggle is set */ +.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output, +.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output { + display: block; + position: static; + width: unset; + background: unset; /* Override the backgrounds set in floating in windowed mode */ + padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */ +} + +.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps, +.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output .goal-hyps { + /* Overridden back in windowed style */ + flex-flow: row wrap; + justify-content: flex-start; +} + +.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div, +.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div { + display: block; +} + +.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-hyps { + display: flex; +} + +.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion { + max-height: unset; + overflow-y: unset; +} + +.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence > .alectryon-toggle ~ .alectryon-wsp, +.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-wsp { + display: none; +} + +.alectryon-io .alectryon-messages, +.alectryon-io .alectryon-message, +.alectryon-io .alectryon-goals, +.alectryon-io .alectryon-goal, +.alectryon-io .goal-hyps > span, +.alectryon-io .goal-conclusion { + border-radius: 0.15em; +} + +.alectryon-io .alectryon-goal, +.alectryon-io .alectryon-message { + align-items: center; + background: #d3d7cf; + display: block; + flex-direction: column; + margin: 0.25em; + padding: 0.5em; + position: relative; +} + +.alectryon-io .goal-hyps { + align-content: space-around; + align-items: baseline; + display: flex; + flex-flow: column nowrap; /* re-stated in windowed mode */ + justify-content: space-around; + /* LATER use a ‘gap’ property instead of margins once supported */ + margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */ + padding-bottom: 0.35em; /* 0.5em-0.15em to cancel the 0.5em of .goal-separator */ +} + +.alectryon-io .goal-hyps > br { + display: none; /* Only for RSS readers */ +} + +.alectryon-io .goal-hyps > span, +.alectryon-io .goal-conclusion { + background: #eeeeec; + display: inline-block; + padding: 0.15em 0.35em; +} + +.alectryon-io .goal-hyps > span { + align-items: baseline; + display: inline-flex; + margin: 0.15em 0.25em; +} + +.alectryon-block var, +.alectryon-inline var, +.alectryon-io .goal-hyps > span > var { + font-weight: 600; + font-style: unset; +} + +.alectryon-io .goal-hyps > span > var { + /* Shrink the list of names, but let it grow as long as space is available. */ + flex-basis: min-content; + flex-grow: 1; +} + +.alectryon-io .goal-hyps > span b { + font-weight: 600; + margin: 0 0 0 0.5em; + white-space: pre; +} + +.alectryon-io .hyp-body, +.alectryon-io .hyp-type { + display: flex; + align-items: baseline; +} + +.alectryon-io .goal-separator { + align-items: center; + display: flex; + flex-direction: row; + height: 1em; /* Fixed height to ignore goal name and markers */ + margin-top: -0.5em; /* Compensated in .goal-hyps when shown */ +} + +.alectryon-io .goal-separator hr { + border: none; + border-top: thin solid #555753; + display: block; + flex-grow: 1; + margin: 0; +} + +.alectryon-io .goal-separator .goal-name { + font-size: 0.75em; + margin-left: 0.5em; +} + +/**********/ +/* Banner */ +/**********/ + +.alectryon-banner { + background: #eeeeec; + border: 1px solid #babcbd; + font-size: 0.75em; + padding: 0.25em; + text-align: center; + margin: 1em 0; +} + +.alectryon-banner a { + cursor: pointer; + text-decoration: underline; +} + +.alectryon-banner kbd { + background: #d3d7cf; + border-radius: 0.15em; + border: 1px solid #babdb6; + box-sizing: border-box; + display: inline-block; + font-family: inherit; + font-size: 0.9em; + height: 1.3em; + line-height: 1.2em; + margin: -0.25em 0; + padding: 0 0.25em; + vertical-align: middle; +} + +/**********/ +/* Toggle */ +/**********/ + +.alectryon-toggle-label { + margin: 1rem 0; +} + +/******************/ +/* Floating style */ +/******************/ + +/* If there's space, display goals to the right of the code, not below it. */ +@media (min-width: 80rem) { + /* Unlike the windowed case, we don't want to move output blocks to the side + when they are both :checked and -targeted, since it gets confusing as + things jump around; hence the commented-output part of the selector, + which would otherwise increase specificity */ + .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output, + .alectryon-floating .alectryon-sentence:hover .alectryon-output { + top: 0; + left: 100%; + right: -100%; + padding: 0 0.5em; + position: absolute; + } + + .alectryon-floating .alectryon-output { + min-height: 100%; + } + + .alectryon-floating .alectryon-sentence:hover .alectryon-output { + background: white; /* Ensure that short goals hide long ones */ + } + + /* This odd margin-bottom property prevents the sticky div from bumping + against the bottom of its container (.alectryon-output). The alternative + would be enlarging .alectryon-output, but that would cause overflows, + enlarging scrollbars and yielding scrolling towards the bottom of the + page. Doing things this way instead makes it possible to restrict + .alectryon-output to a reasonable size (100%, through top = bottom = 0). + See also https://stackoverflow.com/questions/43909940/. */ + /* See note on specificity above */ + .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output > div, + .alectryon-floating .alectryon-sentence:hover .alectryon-output > div { + margin-bottom: -200%; + position: sticky; + top: 0; + } + + .alectryon-floating .alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div, + .alectryon-floating .alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div { + margin-bottom: unset; /* Undo the margin */ + } + + /* Float underneath the current fragment + @media (max-width: 80rem) { + .alectryon-floating .alectryon-output { + top: 100%; + } + } */ +} + +/********************/ +/* Multi-pane style */ +/********************/ + +.alectryon-windowed { + border: 0 solid #2e3436; + box-sizing: border-box; +} + +.alectryon-windowed .alectryon-sentence:hover .alectryon-output { + background: white; /* Ensure that short goals hide long ones */ +} + +.alectryon-windowed .alectryon-output { + position: fixed; /* Overwritten by the ‘:checked’ rules */ +} + +/* See note about specificity below */ +.alectryon-windowed .alectryon-sentence:hover .alectryon-output, +.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output { + padding: 0.5em; + overflow-y: auto; /* Windowed contents may need to scroll */ +} + +.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages, +.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-messages, +.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals, +.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-goals { + box-shadow: none; /* A shadow is unnecessary here and incompatible with overflow-y set to auto */ +} + +.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .goal-hyps { + /* Restated to override the :checked style */ + flex-flow: column nowrap; + justify-content: space-around; +} + + +.alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-extra-goals .alectryon-goal .goal-conclusion +/* Like .alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion */ { + max-height: unset; + overflow-y: unset; +} + +.alectryon-windowed .alectryon-output > div { + display: flex; /* Put messages after goals */ + flex-direction: column-reverse; +} + +/*********************/ +/* Standalone styles */ +/*********************/ + +.alectryon-standalone { + font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif; + line-height: 1.5; +} + +@media screen and (min-width: 50rem) { + html.alectryon-standalone { + /* Prevent flickering when hovering a block causes scrollbars to appear. */ + margin-left: calc(100vw - 100%); + margin-right: 0; + } +} + +/* Coqdoc */ + +.alectryon-coqdoc .doc .code, +.alectryon-coqdoc .doc .inlinecode, +.alectryon-coqdoc .doc .comment { + display: inline; +} + +.alectryon-coqdoc .doc .comment { + color: #eeeeec; +} + +.alectryon-coqdoc .doc .paragraph { + height: 0.75em; +} + +/* Centered, Floating */ + +.alectryon-standalone .alectryon-centered, +.alectryon-standalone .alectryon-floating { + max-width: 50rem; + margin: auto; +} + +@media (min-width: 80rem) { + .alectryon-standalone .alectryon-floating { + max-width: 80rem; + } + + .alectryon-standalone .alectryon-floating > * { + width: 50%; + margin-left: 0; + } +} + +/* Windowed */ + +.alectryon-standalone .alectryon-windowed { + display: block; + margin: 0; + overflow-y: auto; + position: absolute; + padding: 0 1em; +} + +.alectryon-standalone .alectryon-windowed > * { + /* Override properties of docutils_basic.css */ + margin-left: 0; + max-width: unset; +} + +.alectryon-standalone .alectryon-windowed .alectryon-io { + box-sizing: border-box; + width: 100%; +} + +/* No need to predicate the ‘:hover’ rules below on ‘:not(:checked)’, since ‘left’, + ‘right’, ‘top’, and ‘bottom’ will be inactived by the :checked rules setting + ‘position’ to ‘static’ */ + + +/* Specificity: We want the output to stay inline when hovered while unfolded + (:checked), but we want it to move when it's targeted (i.e. when the user + is browsing goals one by one using the keyboard, in which case we want to + goals to appear in consistent locations). The selectors below ensure + that :hover < :checked < -targeted in terms of specificity. */ +/* LATER: Reimplement this stuff with CSS variables */ +.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output { + position: fixed; +} + +@media screen and (min-width: 60rem) { + .alectryon-standalone .alectryon-windowed { + border-right-width: thin; + bottom: 0; + left: 0; + right: 50%; + top: 0; + } + + .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output, + .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output { + bottom: 0; + left: 50%; + right: 0; + top: 0; + } +} + +@media screen and (max-width: 60rem) { + .alectryon-standalone .alectryon-windowed { + border-bottom-width: 1px; + bottom: 40%; + left: 0; + right: 0; + top: 0; + } + + .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output, + .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output { + bottom: 0; + left: 0; + right: 0; + top: 60%; + } +} diff --git a/doc/alectryon.js b/doc/alectryon.js new file mode 100644 index 0000000000..d503e0fd24 --- /dev/null +++ b/doc/alectryon.js @@ -0,0 +1,190 @@ +var Alectryon; +(function(Alectryon) { + (function (slideshow) { + function anchor(sentence) { return "#" + sentence.id; } + + function current_sentence() { return slideshow.sentences[slideshow.pos]; } + + function unhighlight() { + var sentence = current_sentence(); + if (sentence) sentence.classList.remove("alectryon-target"); + slideshow.pos = -1; + } + + function highlight(sentence) { + sentence.classList.add("alectryon-target"); + } + + function scroll(sentence) { + // Put the top of the current fragment close to the top of the + // screen, but scroll it out of view if showing it requires pushing + // the sentence past half of the screen. If sentence is already in + // a reasonable position, don't move. + var parent = sentence.parentElement; + /* We want to scroll the whole document, so start at root… */ + while (parent && !parent.classList.contains("alectryon-root")) + parent = parent.parentElement; + /* … and work up from there to find a scrollable element. + parent.scrollHeight can be greater than parent.clientHeight + without showing scrollbars, so we add a 10px buffer. */ + while (parent && parent.scrollHeight <= parent.clientHeight + 10) + parent = parent.parentElement; + /* and elements can have their client rect overflow + * the window if their height is unset, so scroll the window + * instead */ + if (parent && (parent.nodeName == "BODY" || parent.nodeName == "HTML")) + parent = null; + + var rect = function(e) { return e.getBoundingClientRect(); }; + var parent_box = parent ? rect(parent) : { y: 0, height: window.innerHeight }, + sentence_y = rect(sentence).y - parent_box.y, + fragment_y = rect(sentence.parentElement).y - parent_box.y; + + // The assertion below sometimes fails for the first element in a block. + // console.assert(sentence_y >= fragment_y); + + if (sentence_y < 0.1 * parent_box.height || + sentence_y > 0.7 * parent_box.height) { + (parent || window).scrollBy( + 0, Math.max(sentence_y - 0.5 * parent_box.height, + fragment_y - 0.1 * parent_box.height)); + } + } + + function highlighted(pos) { + return slideshow.pos == pos; + } + + function navigate(pos, inhibitScroll) { + unhighlight(); + slideshow.pos = Math.min(Math.max(pos, 0), slideshow.sentences.length - 1); + var sentence = current_sentence(); + highlight(sentence); + if (!inhibitScroll) + scroll(sentence); + } + + var keys = { + PAGE_UP: 33, + PAGE_DOWN: 34, + ARROW_UP: 38, + ARROW_DOWN: 40, + h: 72, l: 76, p: 80, n: 78 + }; + + function onkeydown(e) { + e = e || window.event; + if (e.ctrlKey || e.metaKey) { + if (e.keyCode == keys.ARROW_UP) + slideshow.previous(); + else if (e.keyCode == keys.ARROW_DOWN) + slideshow.next(); + else + return; + } else { + // if (e.keyCode == keys.PAGE_UP || e.keyCode == keys.p || e.keyCode == keys.h) + // slideshow.previous(); + // else if (e.keyCode == keys.PAGE_DOWN || e.keyCode == keys.n || e.keyCode == keys.l) + // slideshow.next(); + // else + return; + } + e.preventDefault(); + } + + function start() { + slideshow.navigate(0); + } + + function toggleHighlight(idx) { + if (highlighted(idx)) + unhighlight(); + else + navigate(idx, true); + } + + function handleClick(evt) { + if (evt.ctrlKey || evt.metaKey) { + var sentence = evt.currentTarget; + + // Ensure that the goal is shown on the side, not inline + var checkbox = sentence.getElementsByClassName("alectryon-toggle")[0]; + if (checkbox) + checkbox.checked = false; + + toggleHighlight(sentence.alectryon_index); + evt.preventDefault(); + } + } + + function init() { + document.onkeydown = onkeydown; + slideshow.pos = -1; + slideshow.sentences = Array.from(document.getElementsByClassName("alectryon-sentence")); + slideshow.sentences.forEach(function (s, idx) { + s.addEventListener('click', handleClick, false); + s.alectryon_index = idx; + }); + } + + slideshow.start = start; + slideshow.end = unhighlight; + slideshow.navigate = navigate; + slideshow.next = function() { navigate(slideshow.pos + 1); }; + slideshow.previous = function() { navigate(slideshow.pos + -1); }; + window.addEventListener('DOMContentLoaded', init); + })(Alectryon.slideshow || (Alectryon.slideshow = {})); + + (function (styles) { + var styleNames = ["centered", "floating", "windowed"]; + + function className(style) { + return "alectryon-" + style; + } + + function setStyle(style) { + var root = document.getElementsByClassName("alectryon-root")[0]; + styleNames.forEach(function (s) { + root.classList.remove(className(s)); }); + root.classList.add(className(style)); + } + + function init() { + var banner = document.getElementsByClassName("alectryon-banner")[0]; + if (banner) { + banner.append(" Style: "); + styleNames.forEach(function (styleName, idx) { + var s = styleName; + var a = document.createElement("a"); + a.onclick = function() { setStyle(s); }; + a.append(styleName); + if (idx > 0) banner.append("; "); + banner.appendChild(a); + }); + banner.append("."); + } + } + + window.addEventListener('DOMContentLoaded', init); + + styles.setStyle = setStyle; + })(Alectryon.styles || (Alectryon.styles = {})); +})(Alectryon || (Alectryon = {})); + +function setHidden(elements, isVisible, token) { + for (let i = 0; i < elements.length; i++) { + if (isVisible) { + elements[i].classList.remove(token) + } else { + elements[i].classList.add(token) + } + } +} + +function toggleShowTypes(checkbox) { + setHidden(document.getElementsByClassName("alectryon-io"), checkbox.checked, "type-info-hidden") +} + +function toggleShowGoals(checkbox) { + setHidden(document.getElementsByClassName("alectryon-io"), checkbox.checked, "output-hidden") +} \ No newline at end of file diff --git a/doc/book.toml b/doc/book.toml index 1c8634d5b7..741aacf707 100644 --- a/doc/book.toml +++ b/doc/book.toml @@ -10,6 +10,8 @@ build-dir = "out" [output.html] git-repository-url = "https://github.com/leanprover/lean4" +additional-css = ["alectryon.css", "pygments.css"] +additional-js = ["alectryon.js"] [output.html.playground.boring-prefixes] lean = "# " diff --git a/doc/examples.md b/doc/examples.md index 2460d1aefb..cdecaae835 100644 --- a/doc/examples.md +++ b/doc/examples.md @@ -1,9 +1,9 @@ Examples ======== -- [Palindromes](examples/palindromes.lean.html) -- [Binary Search Trees](examples/bintree.lean.html) -- [A Certified Type Checker](examples/tc.lean.html) -- [The Well-Typed Interpreter](examples/interp.lean.html) -- [Dependent de Bruijn Indices](examples/deBruijn.lean.html) -- [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.html) +- [Palindromes](examples/palindromes.lean.md) +- [Binary Search Trees](examples/bintree.lean.md) +- [A Certified Type Checker](examples/tc.lean.md) +- [The Well-Typed Interpreter](examples/interp.lean.md) +- [Dependent de Bruijn Indices](examples/deBruijn.lean.md) +- [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.md) diff --git a/doc/examples/bintree.lean.md b/doc/examples/bintree.lean.md new file mode 100644 index 0000000000..a9584d5478 --- /dev/null +++ b/doc/examples/bintree.lean.md @@ -0,0 +1,5 @@ +(this example is rendered by Alectryon in the CI) + +```lean +{{#include bintree.lean}} +``` diff --git a/doc/examples/deBruijn.lean.md b/doc/examples/deBruijn.lean.md new file mode 100644 index 0000000000..6a0b8c5060 --- /dev/null +++ b/doc/examples/deBruijn.lean.md @@ -0,0 +1,5 @@ +(this example is rendered by Alectryon in the CI) + +```lean +{{#include deBruijn.lean}} +``` diff --git a/doc/examples/interp.lean.md b/doc/examples/interp.lean.md new file mode 100644 index 0000000000..d6989e2d83 --- /dev/null +++ b/doc/examples/interp.lean.md @@ -0,0 +1,5 @@ +(this example is rendered by Alectryon in the CI) + +```lean +{{#include interp.lean}} +``` diff --git a/doc/examples/palindromes.lean.md b/doc/examples/palindromes.lean.md new file mode 100644 index 0000000000..453239f4d7 --- /dev/null +++ b/doc/examples/palindromes.lean.md @@ -0,0 +1,5 @@ +(this example is rendered by Alectryon in the CI) + +```lean +{{#include palindromes.lean}} +``` diff --git a/doc/examples/phoas.lean.md b/doc/examples/phoas.lean.md new file mode 100644 index 0000000000..938a42c41d --- /dev/null +++ b/doc/examples/phoas.lean.md @@ -0,0 +1,5 @@ +(this example is rendered by Alectryon in the CI) + +```lean +{{#include phoas.lean}} +``` diff --git a/doc/examples/tc.lean.md b/doc/examples/tc.lean.md new file mode 100644 index 0000000000..4de865d0cb --- /dev/null +++ b/doc/examples/tc.lean.md @@ -0,0 +1,5 @@ +(this example is rendered by Alectryon in the CI) + +```lean +{{#include tc.lean}} +``` diff --git a/doc/flake.lock b/doc/flake.lock index 57d8265618..0bffec8151 100644 --- a/doc/flake.lock +++ b/doc/flake.lock @@ -3,15 +3,15 @@ "alectryon-src": { "flake": false, "locked": { - "lastModified": 1646696858, - "narHash": "sha256-XdqpyXFv2KVGwgn9KGtOBUocobrnnXXZeiDIGSpo/IE=", - "owner": "insightmind", + "lastModified": 1648983871, + "narHash": "sha256-Xenmtxe/wZBq4xI+jd45IezINWVvY3aoBLuwrzV5ZEQ=", + "owner": "Kha", "repo": "alectryon", - "rev": "0c99a16df8ac2c500a21371629f63d011da7ef19", + "rev": "6ec91785a9076c45695c8efcc92225a05832242d", "type": "github" }, "original": { - "owner": "insightmind", + "owner": "Kha", "ref": "typeid", "repo": "alectryon", "type": "github" diff --git a/doc/flake.nix b/doc/flake.nix index 669f6dce5b..59d7f36211 100644 --- a/doc/flake.nix +++ b/doc/flake.nix @@ -8,7 +8,7 @@ flake = false; }; inputs.alectryon-src = { - url = github:insightmind/alectryon/typeid; + url = github:Kha/alectryon/typeid; flake = false; }; inputs.leanInk-src = { @@ -36,7 +36,12 @@ src = doc-src; buildInputs = [ lean-mdbook ]; buildCommand = '' - mdbook build -d $out $src/doc + mkdir $out + # necessary for `additional-css`...? + cp -r --no-preserve=mode $src/doc/* . + # overwrite stub .lean.md files + cp -r ${examples}/* . + mdbook build -d $out ''; }; # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache @@ -70,16 +75,16 @@ doCheck = false; }; examples = let - renderLean = name: file: runCommandNoCC "${name}.html" { buildInputs = [ alectryon ]; } '' + renderLean = name: file: runCommandNoCC "${name}.md" { buildInputs = [ alectryon ]; } '' mkdir -p $out/examples - alectryon --frontend lean4+rst ${file} -o $out/examples/${name}.html + alectryon --frontend lean4+markup ${file} --backend webpage -o $out/examples/${name}.md ''; ents = builtins.readDir ./examples; - inputs = lib.filterAttrs (n: t: t == "regular") ents; + inputs = lib.filterAttrs (n: t: builtins.match ".*\.lean" n != null && t == "regular") ents; outputs = lib.mapAttrs (n: _: renderLean n ./examples/${n}) inputs; in outputs // symlinkJoin { name = "examples"; paths = lib.attrValues outputs; }; - doc = symlinkJoin { name = "doc"; paths = [ book examples ]; }; + doc = book; }; defaultPackage = self.packages.${system}.doc; }); diff --git a/doc/pygments.css b/doc/pygments.css new file mode 100644 index 0000000000..0edad2aea3 --- /dev/null +++ b/doc/pygments.css @@ -0,0 +1,81 @@ +/* Pygments stylesheet generated by Alectryon (style=None) */ +td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; } +span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; } +td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; } +span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; } +.highlight .hll, .code .hll { background-color: #ffffcc } +.highlight .c, .code .c { color: #555753; font-style: italic } /* Comment */ +.highlight .err, .code .err { color: #a40000; border: 1px solid #cc0000 } /* Error */ +.highlight .g, .code .g { color: #000000 } /* Generic */ +.highlight .k, .code .k { color: #8f5902 } /* Keyword */ +.highlight .l, .code .l { color: #2e3436 } /* Literal */ +.highlight .n, .code .n { color: #000000 } /* Name */ +.highlight .o, .code .o { color: #000000 } /* Operator */ +.highlight .x, .code .x { color: #2e3436 } /* Other */ +.highlight .p, .code .p { color: #000000 } /* Punctuation */ +.highlight .ch, .code .ch { color: #555753; font-weight: bold; font-style: italic } /* Comment.Hashbang */ +.highlight .cm, .code .cm { color: #555753; font-style: italic } /* Comment.Multiline */ +.highlight .cp, .code .cp { color: #3465a4; font-style: italic } /* Comment.Preproc */ +.highlight .cpf, .code .cpf { color: #555753; font-style: italic } /* Comment.PreprocFile */ +.highlight .c1, .code .c1 { color: #555753; font-style: italic } /* Comment.Single */ +.highlight .cs, .code .cs { color: #3465a4; font-weight: bold; font-style: italic } /* Comment.Special */ +.highlight .gd, .code .gd { color: #a40000 } /* Generic.Deleted */ +.highlight .ge, .code .ge { color: #000000; font-style: italic } /* Generic.Emph */ +.highlight .gr, .code .gr { color: #a40000 } /* Generic.Error */ +.highlight .gh, .code .gh { color: #a40000; font-weight: bold } /* Generic.Heading */ +.highlight .gi, .code .gi { color: #4e9a06 } /* Generic.Inserted */ +.highlight .go, .code .go { color: #000000; font-style: italic } /* Generic.Output */ +.highlight .gp, .code .gp { color: #8f5902 } /* Generic.Prompt */ +.highlight .gs, .code .gs { color: #000000; font-weight: bold } /* Generic.Strong */ +.highlight .gu, .code .gu { color: #000000; font-weight: bold } /* Generic.Subheading */ +.highlight .gt, .code .gt { color: #000000; font-style: italic } /* Generic.Traceback */ +.highlight .kc, .code .kc { color: #204a87; font-weight: bold } /* Keyword.Constant */ +.highlight .kd, .code .kd { color: #4e9a06; font-weight: bold } /* Keyword.Declaration */ +.highlight .kn, .code .kn { color: #4e9a06; font-weight: bold } /* Keyword.Namespace */ +.highlight .kp, .code .kp { color: #204a87 } /* Keyword.Pseudo */ +.highlight .kr, .code .kr { color: #8f5902 } /* Keyword.Reserved */ +.highlight .kt, .code .kt { color: #204a87 } /* Keyword.Type */ +.highlight .ld, .code .ld { color: #2e3436 } /* Literal.Date */ +.highlight .m, .code .m { color: #2e3436 } /* Literal.Number */ +.highlight .s, .code .s { color: #ad7fa8 } /* Literal.String */ +.highlight .na, .code .na { color: #c4a000 } /* Name.Attribute */ +.highlight .nb, .code .nb { color: #75507b } /* Name.Builtin */ +.highlight .nc, .code .nc { color: #204a87 } /* Name.Class */ +.highlight .no, .code .no { color: #ce5c00 } /* Name.Constant */ +.highlight .nd, .code .nd { color: #3465a4; font-weight: bold } /* Name.Decorator */ +.highlight .ni, .code .ni { color: #c4a000; text-decoration: underline } /* Name.Entity */ +.highlight .ne, .code .ne { color: #cc0000 } /* Name.Exception */ +.highlight .nf, .code .nf { color: #a40000 } /* Name.Function */ +.highlight .nl, .code .nl { color: #3465a4; font-weight: bold } /* Name.Label */ +.highlight .nn, .code .nn { color: #000000 } /* Name.Namespace */ +.highlight .nx, .code .nx { color: #000000 } /* Name.Other */ +.highlight .py, .code .py { color: #000000 } /* Name.Property */ +.highlight .nt, .code .nt { color: #a40000 } /* Name.Tag */ +.highlight .nv, .code .nv { color: #ce5c00 } /* Name.Variable */ +.highlight .ow, .code .ow { color: #8f5902 } /* Operator.Word */ +.highlight .w, .code .w { color: #d3d7cf; text-decoration: underline } /* Text.Whitespace */ +.highlight .mb, .code .mb { color: #2e3436 } /* Literal.Number.Bin */ +.highlight .mf, .code .mf { color: #2e3436 } /* Literal.Number.Float */ +.highlight .mh, .code .mh { color: #2e3436 } /* Literal.Number.Hex */ +.highlight .mi, .code .mi { color: #2e3436 } /* Literal.Number.Integer */ +.highlight .mo, .code .mo { color: #2e3436 } /* Literal.Number.Oct */ +.highlight .sa, .code .sa { color: #ad7fa8 } /* Literal.String.Affix */ +.highlight .sb, .code .sb { color: #ad7fa8 } /* Literal.String.Backtick */ +.highlight .sc, .code .sc { color: #ad7fa8; font-weight: bold } /* Literal.String.Char */ +.highlight .dl, .code .dl { color: #ad7fa8 } /* Literal.String.Delimiter */ +.highlight .sd, .code .sd { color: #ad7fa8 } /* Literal.String.Doc */ +.highlight .s2, .code .s2 { color: #ad7fa8 } /* Literal.String.Double */ +.highlight .se, .code .se { color: #ad7fa8; font-weight: bold } /* Literal.String.Escape */ +.highlight .sh, .code .sh { color: #ad7fa8; text-decoration: underline } /* Literal.String.Heredoc */ +.highlight .si, .code .si { color: #ce5c00 } /* Literal.String.Interpol */ +.highlight .sx, .code .sx { color: #ad7fa8 } /* Literal.String.Other */ +.highlight .sr, .code .sr { color: #ad7fa8 } /* Literal.String.Regex */ +.highlight .s1, .code .s1 { color: #ad7fa8 } /* Literal.String.Single */ +.highlight .ss, .code .ss { color: #8f5902 } /* Literal.String.Symbol */ +.highlight .bp, .code .bp { color: #5c35cc } /* Name.Builtin.Pseudo */ +.highlight .fm, .code .fm { color: #a40000 } /* Name.Function.Magic */ +.highlight .vc, .code .vc { color: #ce5c00 } /* Name.Variable.Class */ +.highlight .vg, .code .vg { color: #ce5c00; text-decoration: underline } /* Name.Variable.Global */ +.highlight .vi, .code .vi { color: #ce5c00 } /* Name.Variable.Instance */ +.highlight .vm, .code .vm { color: #ce5c00 } /* Name.Variable.Magic */ +.highlight .il, .code .il { color: #2e3436 } /* Literal.Number.Integer.Long */ \ No newline at end of file