diff --git a/admin/site/content/about.md b/admin/site/content/about.md --- a/admin/site/content/about.md +++ b/admin/site/content/about.md @@ -1,54 +1,54 @@ --- title: "About" menu: main: name: "About" weight: 6 --- The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal. -[Submissions](/contribution) are refereed. +[Submissions](/submission) are refereed. The archive repository is hosted on [Heptapod](https://foss.heptapod.net/isa-afp/) to provide easy free access to archive entries. The entries are tested and maintained continuously against the current stable release of Isabelle. Older versions of archive entries will remain available. ## Editors The editors of the Archive of Formal Proofs are: * [Manuel Eberl](http://www.in.tum.de/~eberlm/), [Technische Universität München](http://www.tum.de/) * [Gerwin Klein](http://www.cse.unsw.edu.au/~kleing/), [Data61](http://www.data61.csiro.au) * [Tobias Nipkow](http://www.in.tum.de/~nipkow/), [Technische Universität München](http://www.tum.de/) * [Larry Paulson](http://www.cl.cam.ac.uk/users/lcp/), [University of Cambridge](http://www.cam.ac.uk/) * [René Thiemann](http://cl-informatik.uibk.ac.at/users/thiemann/), [University of Innsbruck](https://www.uibk.ac.at/) ## Why We aim to strengthen the community and to foster the development of formal proofs. We hope that the Archive will provide: * a resource of knowledge, examples, and libraries for users, * a large and relevant test bed of theories for Isabelle developers, and * a central, citable place for authors to publish their theories We encourage authors of publications that contain Isabelle developments to make their theories available in the Archive of Formal Proofs and to refer to the archive entry in their publication. It makes it easier for referees to check the validity of theorems (all entries in the Archive are mechanically checked), it makes it easier for readers of the publication to understand details of your development, and it makes it easier to use and build on your work. ## License All entries in the Archive of Formal Proofs are licensed under a [BSD-style License](LICENSE) or the [GNU LGPL](http://www.gnu.org/copyleft/lesser.html). This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions. The authors retain their full copyright on their original work, including their right to make the development available under another, additional license in the future. ## Website This website is the result of a project from the School of Informatics at the [University of Edinburgh](https://www.ed.ac.uk) by: * Carlin MacKenzie * James Vaughan, [AIML](https://aiml.inf.ed.ac.uk) * Jacques Fleuriot, [AIAI](http://web.inf.ed.ac.uk/aiai/) Integration and maintenance by: * [Fabian Huch](https://www21.in.tum.de/team/huch), [Technische Universität München](http://www.tum.de/) diff --git a/admin/site/content/contribution.md b/admin/site/content/contribution.md deleted file mode 100644 --- a/admin/site/content/contribution.md +++ /dev/null @@ -1,63 +0,0 @@ ---- -title: Contribution -menu: - bottom: - name: "Contribution" ---- - -## Submission Guidelines - -**The submission must follow the following Isabelle style rules.** For additional guidelines on Isabelle proofs, also see the this [guide](http://proofcraft.org/blog/isabelle-style.html) (feel free to follow all of these; only the below are mandatory). **Technical details about the submission process and the format of the submission are explained on the submission site.** - -* No use of the commands `sorry` or `back`. -* Instantiations must not use Isabelle-generated names such as `xa` — use Isar, the `subgoal` command or `rename_tac` to avoid such names. -* No use of the command `smt_oracle`. -* If your theories contain calls to `nitpick`, `quickcheck`, or `nunchaku` those calls must include the `expect` parameter. Alternatively the `expect` parameter must be set globally via, e.g. `nitpick_params`. -* `apply` scripts should be indented by subgoal as in the Isabelle distribution. If an `apply` command is applied to a state with `n+1` subgoals, it must be indented by `n` spaces relative to the first `apply` in the sequence. -* Only named lemmas should carry attributes such as `[simp]`. -* We prefer structured Isar proofs over apply style, but do not mandate them. -* If there are proof steps that take significant time, i.e. longer than roughly 1 min, please add a short comment to that step, so maintainers will know what to expect. -* The entry must contain a ROOT file with one session that has the name of the entry. We strongly encourage precisely one session per entry, but exceptions can be made. All sessions must be in group (AFP), and all theory files of the submission must be contained in at least one session. See also the example [ROOT](https://foss.heptapod.net/isa-afp/afp-2020/-/blob/branch/default/thys/Example-Submission/ROOT) file in the [Example submission](/entries/Example-Submission.html). -* The entry should cite all sources that the theories are based on, for example textbooks or research articles containing informal versions of the proofs. - -Your submission must contain an abstract to be displayed on the web site – usually this will be the same as the abstract of your proof document in the root.tex file. You can use LaTeX formulae in this web site abstract, either inline formulae in the form $a+b$ or \\(a+b\\) or display formulae in the form $$a + b$$ or \\\[a + b\\\]. Other occurrences of these characters must be escaped (e.g. \\$ or \\\\(). Note that LaTeX in the title of an entry is _not_ allowed. Most basic LaTeX functionality should be supported. For details on what parts of LaTeX are supported, see the [MathJax documentation.](https://docs.mathjax.org/en/v2.7-latest/tex.html) - -It is possible and encouraged to build on other archive entries in your submission. There is a standardised way to [refer to other AFP entries](/help) in your theories. - -## Submission Form - -Please send your submission [via this web page](https://ci.isabelle.systems/afp-submission/). - -Your submission will be refereed and you will receive notification as soon as possible. If accepted, you must agree to maintain your archive entry or nominate someone else to maintain it. The Isabelle development team will assist with maintenance, but it does not have the resources to fully maintain the complete archive. - -If you have questions regarding your submission, please email [afp-submit@in.tum.de](mailto:afp-submit@in.tum.de). If you need help with Isabelle, please use the [isabelle-users@cl.cam.ac.uk](mailto:isabelle-users@cl.cam.ac.uk) mailing list. It is always a good idea to [subscribe](https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users). - -# Updating Entries - -## Change - -The Archive of Formal Proofs is an online resource and therefore more dynamic than a normal scientific journal. Existing entries can and do evolve and can also be updated significantly by their authors. - -This conflicts with the purpose of archiving and preserving entries as they have been submitted and with the purpose of providing a clear and simple interface to readers. - -The AFP deals with this by synchronizing such updates with Isabelle releases: - -* The entries released and visible on the main site are always working with the most recent stable Isabelle version and do not change. -* In the background, the archive maintainers evolve all entries to be up to date with the current Isabelle development version. Authors can contribute changes to this version which is available as a [Heptapod mercurial repository](https://foss.heptapod.net/isa-afp/afp-devel/) or as tar.gz package on the [download page](/download). -* When a new Isabelle version is released, the above mentioned development version of AFP is frozen and turns into the main version displayed on the front page. Older versions (including the original submission) of all entries are archived and remain accessible. - -Significant changes of an entry should be recorded in the metadata of the entry using the keyword "extra-history". The resulting web page should look [something like this](https://www.isa-afp.org/entries/JinjaThreads.html). - -## Monotonicity - -Updating an entry should be mostly monotone: you add new material, but you do not modify existing material in a major way. Ideally, entries (by other people) that build on yours should not be affected. Otherwise you have to liaise with them first. If you intend to carry out major non-monotone changes, you will need to submit a completely new entry (with a description of how it relates to the old one). This should be required only very rarely: AFP entries should be mature enough not to require major changes to their interface (i.e. the main functions and theorems provided). - -Major monotone changes, e.g. adding a new concept rather than more results on existing concepts, may also call for a new entry, but one that builds on the existing one. This depends on how you would like to organize your entries. - -## If you are an author - -The above means that if you are an author and would like to provide a new, better version of your AFP entry, you can do so. - -To achieve this, you should base your changes on the [mercurial development version](https:/foss.heptapod.net/isa-afp/afp-devel/) of your AFP entry and test it against the current [Isabelle development version](http://isabelle.in.tum.de/devel/). - -If you would like to get write access to your entry in the mercurial repository or if you need assistance, please contact the [editors](/about#editors). diff --git a/admin/site/content/submission.md b/admin/site/content/submission.md --- a/admin/site/content/submission.md +++ b/admin/site/content/submission.md @@ -1,5 +1,63 @@ --- -title: AFP Submission +title: Entry Submission +menu: + bottom: + name: "Submission" --- -{{< submission >}} \ No newline at end of file +## Submission Guidelines + +**The submission must follow the following Isabelle style rules.** For additional guidelines on Isabelle proofs, also see the this [guide](http://proofcraft.org/blog/isabelle-style.html) (feel free to follow all of these; only the below are mandatory). **Technical details about the submission process and the format of the submission are explained on the submission site.** + +* No use of the commands `sorry` or `back`. +* Instantiations must not use Isabelle-generated names such as `xa` — use Isar, the `subgoal` command or `rename_tac` to avoid such names. +* No use of the command `smt_oracle`. +* If your theories contain calls to `nitpick`, `quickcheck`, or `nunchaku` those calls must include the `expect` parameter. Alternatively the `expect` parameter must be set globally via, e.g. `nitpick_params`. +* `apply` scripts should be indented by subgoal as in the Isabelle distribution. If an `apply` command is applied to a state with `n+1` subgoals, it must be indented by `n` spaces relative to the first `apply` in the sequence. +* Only named lemmas should carry attributes such as `[simp]`. +* We prefer structured Isar proofs over apply style, but do not mandate them. +* If there are proof steps that take significant time, i.e. longer than roughly 1 min, please add a short comment to that step, so maintainers will know what to expect. +* The entry must contain a ROOT file with one session that has the name of the entry. We strongly encourage precisely one session per entry, but exceptions can be made. All sessions must be in group (AFP), and all theory files of the submission must be contained in at least one session. See also the example [ROOT](https://foss.heptapod.net/isa-afp/afp-2020/-/blob/branch/default/thys/Example-Submission/ROOT) file in the [Example submission](/entries/Example-Submission.html). +* The entry should cite all sources that the theories are based on, for example textbooks or research articles containing informal versions of the proofs. + +Your submission must contain an abstract to be displayed on the web site – usually this will be the same as the abstract of your proof document in the root.tex file. You can use LaTeX formulae in this web site abstract, either inline formulae in the form $a+b$ or \\(a+b\\) or display formulae in the form $$a + b$$ or \\\[a + b\\\]. Other occurrences of these characters must be escaped (e.g. \\$ or \\\\(). Note that LaTeX in the title of an entry is _not_ allowed. Most basic LaTeX functionality should be supported. For details on what parts of LaTeX are supported, see the [MathJax documentation.](https://docs.mathjax.org/en/v2.7-latest/tex.html) + +It is possible and encouraged to build on other archive entries in your submission. There is a standardised way to [refer to other AFP entries](/help) in your theories. + +## Submission Form + +Please send your submission [via this web page](https://ci.isabelle.systems/afp-submission/). + +Your submission will be refereed and you will receive notification as soon as possible. If accepted, you must agree to maintain your archive entry or nominate someone else to maintain it. The Isabelle development team will assist with maintenance, but it does not have the resources to fully maintain the complete archive. + +If you have questions regarding your submission, please email [afp-submit@in.tum.de](mailto:afp-submit@in.tum.de). If you need help with Isabelle, please use the [isabelle-users@cl.cam.ac.uk](mailto:isabelle-users@cl.cam.ac.uk) mailing list. It is always a good idea to [subscribe](https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users). + +# Updating Entries + +## Change + +The Archive of Formal Proofs is an online resource and therefore more dynamic than a normal scientific journal. Existing entries can and do evolve and can also be updated significantly by their authors. + +This conflicts with the purpose of archiving and preserving entries as they have been submitted and with the purpose of providing a clear and simple interface to readers. + +The AFP deals with this by synchronizing such updates with Isabelle releases: + +* The entries released and visible on the main site are always working with the most recent stable Isabelle version and do not change. +* In the background, the archive maintainers evolve all entries to be up to date with the current Isabelle development version. Authors can contribute changes to this version which is available as a [Heptapod mercurial repository](https://foss.heptapod.net/isa-afp/afp-devel/) or as tar.gz package on the [download page](/download). +* When a new Isabelle version is released, the above mentioned development version of AFP is frozen and turns into the main version displayed on the front page. Older versions (including the original submission) of all entries are archived and remain accessible. + +Significant changes of an entry should be recorded in the metadata of the entry using the keyword "extra-history". The resulting web page should look [something like this](https://www.isa-afp.org/entries/JinjaThreads.html). + +## Monotonicity + +Updating an entry should be mostly monotone: you add new material, but you do not modify existing material in a major way. Ideally, entries (by other people) that build on yours should not be affected. Otherwise you have to liaise with them first. If you intend to carry out major non-monotone changes, you will need to submit a completely new entry (with a description of how it relates to the old one). This should be required only very rarely: AFP entries should be mature enough not to require major changes to their interface (i.e. the main functions and theorems provided). + +Major monotone changes, e.g. adding a new concept rather than more results on existing concepts, may also call for a new entry, but one that builds on the existing one. This depends on how you would like to organize your entries. + +## If you are an author + +The above means that if you are an author and would like to provide a new, better version of your AFP entry, you can do so. + +To achieve this, you should base your changes on the [mercurial development version](https:/foss.heptapod.net/isa-afp/afp-devel/) of your AFP entry and test it against the current [Isabelle development version](http://isabelle.in.tum.de/devel/). + +If you would like to get write access to your entry in the mercurial repository or if you need assistance, please contact the [editors](/about#editors). diff --git a/admin/site/themes/afp/assets/sass/main.scss b/admin/site/themes/afp/assets/sass/main.scss --- a/admin/site/themes/afp/assets/sass/main.scss +++ b/admin/site/themes/afp/assets/sass/main.scss @@ -1,1109 +1,1073 @@ //colors $theme: hsl(242, 27%, 24%); $theme-hover: hsl(241, 26%, 36%); $theme-lightest: hsl(261, 36%, 86%); $theme-focus: #acabcf; $link: #0645ad; $link-hover: #0000ee; $link-visited: #42047c; $white: #fff; $lightest-grey: #f2f2f2; $lighter-grey: #ddd; $light-grey: #bbb; $dark-grey: #777; $darker-grey: #555; $darkest-grey: #303030; $black: #000; $black_15: rgba(0, 0, 0, 0.15); //fonts $sans-serif: "Open Sans", sans-serif; $monospace: "Consolas", monospace; $OpenSans: "Open Sans"; $light: 300; $normal: 400; $bold: 700; $border-bottom: 2px $darker-grey solid; %code { font-family: $monospace; background-color: $lightest-grey; color: $darkest-grey; } %button { border: 1px solid $dark-grey; font-size: 1rem; vertical-align: middle; background-color: $white; color: $black; line-height: 0; font-family: $sans-serif; } %button-image { position: relative; top: 0.12em; left: 5px; padding-right: 5px; } %sticky { position: sticky; top: 0; background-color: $white; margin: 0; padding-bottom: 0.5rem; } @font-face { font-family: $OpenSans; font-display: swap; font-style: normal; font-weight: 300; src: local(""), url("/font/open-sans-v18-latin-300.woff2") format("woff2"), url("/font/open-sans-v18-latin-300.woff") format("woff"); } @font-face { font-family: $OpenSans; font-display: swap; font-style: normal; font-weight: 400; src: local(""), url("/font/open-sans-v18-latin-regular.woff2") format("woff2"), url("/font/open-sans-v18-latin-regular.woff") format("woff"); } @font-face { font-family: $OpenSans; font-display: swap; font-style: italic; font-weight: 400; src: local(""), url("/font/open-sans-v18-latin-italic.woff2") format("woff2"), url("/font/open-sans-v18-latin-italic.woff") format("woff"); } @font-face { font-family: $OpenSans; font-display: swap; font-style: normal; font-weight: 700; src: local(""), url("/font/open-sans-v18-latin-700.woff2") format("woff2"), url("/font/open-sans-v18-latin-700.woff") format("woff"); } @font-face { font-family: $OpenSans; font-display: swap; font-style: italic; font-weight: 700; src: local(""), url("/font/open-sans-v18-latin-700italic.woff2") format("woff2"), url("/font/open-sans-v18-latin-700italic.woff") format("woff"); } *::selection { background-color: $theme; color: $white; } body { color: $black; background: $white; font-family: $sans-serif; display: grid; grid-template-columns: #{"max(20%, 200px)"} 1fr; grid-template-areas: "sidebar content"; justify-items: center; margin: 0; } aside { grid-area: sidebar; background-color: $theme; width: 20vw; margin: 0; height: 100%; position: fixed; top: 0; left: 0; min-width: 200px; word-break: break-all; overflow-y: auto; color: $white; nav { display: flex; flex-direction: column; justify-content: space-between; height: 100vh; } ul { list-style: none; padding: 0; } li { padding: 0.5em 2rem; &:hover { background-color: $theme-hover; } } .active { background-color: $theme-hover; } div > a { display: block; text-align: center; } a { &:link, &:visited { color: $white; } &:focus { outline: 1px $theme-focus solid; outline-offset: 3.5px; } } hr { margin: 2rem; border: none; border-top: 2px solid $dark-grey; } } .logo { width: 40%; height: auto; padding: 10%; max-width: 160px; } li { margin: 0.25em 0; } header { border-bottom: $border-bottom; margin-bottom: 20px; padding: 0.5rem 0; > div { display: flex; justify-content: space-between; padding: 0.5rem 0; } form { padding: 0.5rem 0; float: right; } h1 { padding: 0.5rem 0; margin: 0; clear: both; line-height: 2.75rem; } #searchInput { height: 2rem; padding: 7px; width: 175px; } #searchButton { height: 2rem; padding: 7px; width: 2rem; &:hover { background-color: $lighter-grey; } &:active { background-color: $light-grey; } } div p { margin: 0; } } .content { grid-area: content; margin: 0 auto 2rem; width: 50vw; min-width: 550px; div { line-height: 1.35em; width: 100%; h1 { border-bottom: $border-bottom; } } > div { form { margin: 2rem auto 0; width: 50%; min-width: 290px; padding: 1rem 0; } #searchButton { height: 2.5rem; width: 25%; min-width: 70px; background: $theme; color: $white; border: 1px $theme solid; } #searchInput { height: 2.5rem; width: 75%; } } .popup { background: $white; box-shadow: 0 0 8px 0 $black_15, 0 4px 10px 0 $black_15; padding: 2.5rem; display: block; width: auto; min-width: 300px; max-width: 90vw; max-height: 75vh; position: fixed; left: 50%; top: 50%; transform: translate(-50%, -50%); overflow-y: auto; } .chart { min-width: 400px; width: 100%; min-height: 400px; max-height: 50vh; background: $white; margin: 20px auto 40px; border: 1px solid $black; position: relative; } .statsnumber { text-align: right; padding-right: 1rem; } ul { list-style-type: none; } li { word-break: break-all; } li::before { content: "–"; position: absolute; margin-left: -1.3em; } } .entries { > div { display: grid; grid-template-columns: 3fr 1fr; } main { padding-right: 2%; max-width: 90ch; div { margin: 1rem 0; } } nav { width: 130px; margin-left: auto; h4 { color: $darker-grey; font-weight: $normal; } } } .theories { grid-template-columns: 20% 80%; justify-content: normal; .collapsible.collapsed { display: none; } .invertible.collapsed { transform: scale(1,-1); } .collapse-container.collapsed { .collapsible { display: none; } .invertible { transform: scale(1,-1); } } .content { min-width: clamp(80ch,50vw, 50vw); width: auto; max-width: 75vw; margin: 0 0 2rem 4vw; } h2 { @extend %sticky; padding-top: 0.5rem; border-bottom: 1px $light-grey solid; svg { height: 2rem; width: 20px; position: absolute; right: 1em; stroke: $dark-grey; transition: transform 100ms; } } main { > div { margin-bottom: 1rem; } } aside { word-break: normal; z-index: 1; overflow-x: hidden; .logo { padding-top: 2rem; padding-bottom: 2rem; width: 100px; @media (min-width: 1800px) { width: 150px; } } > div { margin-right: 1rem; } &:hover { min-width: fit-content; div { min-width: fit-content; } } ul { margin-left: 1.75rem; } li { padding: 0; &:hover { background-color: $theme; } > a:hover { background-color: $theme-hover; } a { padding: 0.5em 0; display: inline-block; width: 100%; } } } @media (max-width: 875px) { padding: 0; grid-template-columns: 1fr; .content { min-width: 350px; max-width: 100vw; margin: 80px 0; } nav { display: none; } } } .links { button { display: inline-block; margin: 0.5rem 0; } a { display: inline-block; margin: 0.5rem 0; } } .popUpButton { &:visited { color: $white; } &:link { border: none; padding: 0.75rem 0; background-color: $theme; color: $white; cursor: pointer; text-align: center; transition: background-color 200ms ease, transform 150ms ease; font-weight: $bold; font-size: 0.9rem; width: 130px; } &:active { transform: scale(0.98); } } a { &:link { color: $link; text-decoration: none; font-weight: $bold; } &:visited { color: $link-visited; } &:hover { color: $link-hover; } } h1 { margin: 1.5em 0 0 0; font-size: 2em; padding-bottom: 20px; span.first { font-size: 2.3rem; } } h2 { margin: 1.5em 0 0 0; padding: 0; line-height: normal; } h3 { margin: 1.5em 0 0 0; font-stretch: normal; font-size: larger; padding: 0; font-weight: $light; &:first-child { margin: 0.5rem 0 0 0; } } h4 { margin: 1.5em 0 0 0; margin-bottom: 0.5ex; font-weight: $bold; } .popup { h2 { margin-top: 0; } .close { position: absolute; width: 20px; height: 20px; top: 2rem; right: 2rem; transition: all 200ms; font-size: 24px; font-weight: $bold; color: $darker-grey; text-align: center; &:hover { color: $darkest-grey; } } } #downloadPopUp { a[download] { display: block; width: 154px; margin: 2.5rem auto 0; } } .year { @extend %sticky; padding-top: 2rem; border-bottom: $border-bottom; } img { max-width: 90%; } pre { @extend %code; padding: 1rem; overflow: auto; &.bibtex { white-space: pre; border-width: thin; border-style: solid; } &.code { white-space: pre; padding: 10px 2px; } } code { padding: 1px 2px 2px; @extend %code; } blockquote { border: 2px solid $lighter-grey; padding: 1rem 2rem; margin: auto 0; } tr:nth-child(even) { background-color: $lightest-grey; } .nobr { white-space: nowrap; } .largeTopMargin { margin-top: 48px; } .searchPage { > div { display: grid; grid-template-columns: 3fr #{"max(25%, 175px)"}; grid-template-rows: 150px 1fr; grid-template-areas: "search search" "entries sidebar"; } form { grid-area: search; } #search-main { grid-area: entries; padding-right: 2rem; box-sizing: border-box; } #search-results { > div { position: relative; margin: 1.5rem 0; border-bottom: 2px $lighter-grey solid; padding-bottom: 1.5rem; } div + div { margin-top: 1rem; } .title, .subtitle { display: flex; justify-content: space-between; align-items: center; } .subtitle { color: $dark-grey; font-size: 0.875em; > p { margin: 0; } } a[download] { padding: 5px 7.5px; flex-shrink: 0; margin-left: 1em; } } #search-sidebar { grid-area: sidebar; } } a[download] { display: inline-block; color: $black; height: 22px; padding: 4px 7px; @extend %button; &:focus { outline: none; box-shadow: 0 0 0 2px #c5c4ddbb; } &:hover, &:active { background-color: $light-grey; color: $black; } &:after { content: url("/images/download.svg"); @extend %button-image; } } .entry { display: flex; align-items: center; margin-top: 1.35rem; a[download] { position: absolute; top: 0; right: 0; } .date { text-align: right; width: 15%; min-width: 6ch; font-family: $monospace; } h5 { font-size: initial; display: initial; } } .form-container { width: 290px; text-align: left; } #searchInput { @extend %button; border-right: none; font-family: $sans-serif; padding: 0.5em; } #searchButton { @extend %button; cursor: pointer; &:focus { outline: none; box-shadow: 0 0 0 2px #c5c4ddbb; } img { max-width: 1rem; } } button { @extend %button; height: 2rem; padding: 7px; font-weight: $bold; cursor: pointer; &:hover { background-color: $lighter-grey; } &:active { background-color: $light-grey; } &:focus { outline: none; box-shadow: 0 0 0 2px #c5c4ddbb; } } button[copy] { &:after { content: url("/images/copy.svg"); @extend %button-image; } } #searchInputautocomplete-list { width: 214px; position: absolute; margin-bottom: 24px; padding: 8px 0; background-color: $white; border: 1px solid $lighter-grey; box-shadow: 0 2px 4px $black_15; z-index: 1; div { width: auto; padding: 8px 12px; line-height: 16px; cursor: pointer; &:hover { background: $lighter-grey; } } } .autocomplete-active { background: $lighter-grey; } .item-text { width: 85%; } .date { color: $darker-grey; font-size: 14px; } .overlay { position: fixed; top: 0; bottom: 0; left: 0; right: 0; background: $black_15; transition: opacity 200ms; visibility: hidden; opacity: 0; .cancel { position: absolute; width: 100%; height: 100%; cursor: pointer; } &:target { visibility: visible; opacity: 1; } } iframe { width: 100%; height: 90vh; } -#banner { - display: block; - background-color: $theme-lightest; - height: 3rem; - width: 80vw; - position: fixed; - bottom: 0; - left: 20vw; - text-align: center; - z-index: 1; - - p { - line-height: 1rem; - } - - button { - height: 1.5rem; - width: 1.5rem; - position: absolute; - right: 2rem; - bottom: 0.75rem; - padding: 0.3rem; - } - - svg { - height: 0.75rem; - width: 0.75rem; - fill: $black; - } - - @media (max-width: 1000px) { - left: 200px; - width: calc(100vw - 200px); - } -} - .loader { margin: 24px 24px 0 0; height: 6px; position: relative; display: block; background-color: $theme; border-radius: 4px; overflow: hidden; .animation { background-color: $light-grey; &:before { content: ''; position: absolute; background-color: inherit; top: 0; left: 0; bottom: 0; will-change: left, right; animation: loader 2s linear infinite; } } } @keyframes loader { 0% { left: -20%; right: 100%; } 100% { left: 100%; right: -20%; } } #menuToggle { input, label { display: none; } > .logoLink, img[alt="Search"] { display: none; } > #menu { box-shadow: 0 .5rem 1rem rgba(0,0,0,.15); } form { display: none; } } @media (max-width: 650px) { .content { width: 90%; min-width: 350px; } .searchPage { > div { display: grid; grid-template-columns: 1fr; grid-template-rows: 150px auto auto ; grid-template-areas: 'search' 'sidebar' 'entries'; } } } @media (max-width: 875px) { body { grid-template-columns: 1fr; grid-template-areas: 'content'; } aside { height: 4rem; width: 100vw; overflow-y: visible; z-index: 1; } header { form { display: none; } } .content { margin-top: 80px; } .entries { > div { display: grid; grid-template-rows: auto auto; grid-template-columns: 1fr; } nav { margin-left: 0; } } .largeTopMargin { margin-top: 0; } #banner { left: 0; width: 100vw; height: 75px; p { line-height: normal; margin: 1rem; } } #menuToggle { background: $theme; display: block; position: relative; top: 0; left: 0; z-index: 1; height: 80px; user-select: none; width: 100vw; a { text-decoration: none; transition: color 0.3s ease; } .logoLink { height: 3rem; max-width: 50vw; top: 1rem; left: 0; right: 0; margin-left: auto; margin-right: auto; img { padding: 0; height: 3rem; object-fit: contain; } } .logoLink, input, label, a[href="/search"] { display: block; position: absolute; z-index: 2; } input, label, a[href="/search"] { width: 24px; height: 24px; top: 28px; } input,label { left: 28px; cursor: pointer; } a[href="/search"] { right: 28px; filter: invert(1); } a[href="/search"] img, label img { width: 100%; } input { opacity: 0; &:checked { ~ nav { left: 0; } } } label span { display: none; } } #menu { height: 100vh; position: absolute; top: 0; left: 0; padding-top: 80px; box-sizing: border-box; min-width: 200px; width: 50vw; max-width: 350px; min-height: 355px; background: $theme; left: -100%; transition: left 0.3s ease; .logoLink { display: none; } } } diff --git a/admin/site/themes/afp/layouts/_default/index.json b/admin/site/themes/afp/layouts/_default/index.json --- a/admin/site/themes/afp/layouts/_default/index.json +++ b/admin/site/themes/afp/layouts/_default/index.json @@ -1,20 +1,26 @@ {{ with $.Scratch.Get "index" }} {{- jsonify . -}} {{ else }} {{- $.Scratch.Add "index" slice -}} - {{- range $index, $element := where .Site.RegularPages "Type" "eq" "entries" -}} + {{- range $index, $element := where .Site.RegularPages "Type" "eq" "entries" -}} + {{- $authors := slice -}} + {{- $data := .Site.Data -}} + {{- range $element.Params.authors -}} + {{- $authors = $authors | append (index (index $data.authors .) "name") -}} + {{- end -}} {{- $.Scratch.Add "index" (dict "id" $index "title" $element.Title "abstract" (replaceRE "\n" " " $element.Params.abstract) "topics" $element.Params.topics "topic_links" (apply $element.Params.topics "urlize" ".") "permalink" $element.Permalink "date" (.Date.Format "2006-01-02") - "authors" $element.Params.authors + "authors" $authors "used_by" (len (index .Site.Taxonomies.dependencies (urlize $element.File.BaseFileName))) - "shortname" $element.File.BaseFileName ) + "shortname" $element.File.BaseFileName + "link" $element.RelPermalink) -}} {{- end -}} {{- $.Scratch.Get "index" | jsonify -}} {{ end }} \ No newline at end of file diff --git a/admin/site/themes/afp/layouts/_default/search.html b/admin/site/themes/afp/layouts/_default/search.html --- a/admin/site/themes/afp/layouts/_default/search.html +++ b/admin/site/themes/afp/layouts/_default/search.html @@ -1,29 +1,29 @@ {{ define "footerfiles" }} {{ end -}} {{- define "main" }} -
+
-
+

Authors

Topics

FindFacts Results

Entries

{{ end }} \ No newline at end of file diff --git a/admin/site/themes/afp/layouts/_default/terms.json b/admin/site/themes/afp/layouts/_default/terms.json --- a/admin/site/themes/afp/layouts/_default/terms.json +++ b/admin/site/themes/afp/layouts/_default/terms.json @@ -1,5 +1,15 @@ {{- $.Scratch.Add "index" slice -}} -{{- range $index, $element := .Data.Pages.ByTitle -}} +{{- if (eq .Section "authors") -}} + {{- range $index, $element := .Data.Pages.ByTitle -}} + {{- $.Scratch.Add "index" (dict + "id" $index + "name" (index (index .Site.Data.authors $element.Name) "name") + "link" $element.Permalink) + -}} + {{- end -}} +{{- else -}} + {{- range $index, $element := .Data.Pages.ByTitle -}} {{- $.Scratch.Add "index" (dict "id" $index "name" $element.Name "link" $element.Permalink) -}} + {{- end -}} {{- end -}} {{- $.Scratch.Get "index" | jsonify -}} \ No newline at end of file diff --git a/admin/site/themes/afp/layouts/entries/single.html b/admin/site/themes/afp/layouts/entries/single.html --- a/admin/site/themes/afp/layouts/entries/single.html +++ b/admin/site/themes/afp/layouts/entries/single.html @@ -1,134 +1,134 @@ {{- define "main" -}} {{- $site := . -}} {{- $path := .Site.Params.afpUrls.html -}} {{- if eq .Site.Params.devel true -}} {{- $path = .Site.Params.afpUrls.htmlDevel -}} {{- end -}} {{- $entry_name := .File.BaseFileName -}}

Abstract

{{- trim .Params.abstract "\n" | safeHTML -}}
{{- if (eq .Params.licence "BSD") -}} BSD License {{- else if (eq .Params.license "LGPL") -}} GNU Lesser General Public License (LGPL) {{- else -}} {{- printf "%s License" .Params.license -}} {{- end -}} {{- with .Params.extra -}} {{- range $key, $value := . -}}

{{- humanize $key -}}

{{- $value | safeHTML -}}

{{- end -}} {{- end -}} {{- $Scratch := newScratch -}} {{- with .Params.dependencies -}}

Depends On

{{- end -}} {{- with (index .Site.Taxonomies.dependencies (urlize $entry_name)) -}}

Used by

{{- end -}} {{- with .Params.topics -}}

Topics

{{- end -}}

Theories

{{ $related := .Site.RegularPages.Related . | first 3 }} {{ with $related }}

Related Entries

{{ end }}

Cite

× 
@article{{- "{" -}}{{- $entry_name -}}-AFP,
   author  = {{ "{" -}}{{- delimit .Params.authors ", " | replaceRE "(, )([^,]+$)" " and $2" -}}},
   title   = {{ "{" -}}{{- htmlUnescape .Params.title -}}},
   journal = {Archive of Formal Proofs},
   month   = {{ dateFormat "January" .Params.date -}},
   year    = {{ dateFormat "2006" .Params.date -}},
   note    = {\url{http://isa-afp.org/entries/{{- $entry_name -}}.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest {{ with .Params.olderReleases -}}

Older releases:

{{- end }}
{{- end -}} diff --git a/admin/site/themes/afp/layouts/index.html b/admin/site/themes/afp/layouts/index.html --- a/admin/site/themes/afp/layouts/index.html +++ b/admin/site/themes/afp/layouts/index.html @@ -1,38 +1,38 @@ {{- define "main" -}}

The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal, is indexed by dblp and has an ISSN: 2150-914x. Submissions are refereed and we encourage companion AFP submissions to conference and journal publications. To cite an entry, please use the preferred citation style.

-
+
{{- range (where site.RegularPages "Type" "in" site.Params.mainSections).GroupByDate "2006" -}}

{{- .Key -}}

{{- range .Pages }}
{{- htmlUnescape .Title -}}

by {{ partial "authors.html" (dict "site" . "authors" .Params.authors) -}}
{{ .Date.Format "Jan 02" }}
{{- end -}}
{{- end -}} {{- end -}} \ No newline at end of file diff --git a/admin/site/themes/afp/layouts/partials/head.html b/admin/site/themes/afp/layouts/partials/head.html --- a/admin/site/themes/afp/layouts/partials/head.html +++ b/admin/site/themes/afp/layouts/partials/head.html @@ -1,69 +1,69 @@ {{- $siteTitle := ( .Site.Title ) -}} {{- if or .IsHome (not .Params.title) -}} {{- $siteTitle -}} {{- else -}} {{- .Params.title | safeHTML }} - {{ $siteTitle -}} {{- end -}} {{- if (eq .Section "entries") -}} {{- else -}} {{- end -}} {{- with .OutputFormats.Get "rss" -}} {{- printf `` .Rel .MediaType.Type .Permalink $.Site.Title | safeHTML -}} {{- end -}} {{- template "_internal/opengraph.html" . -}} {{- template "_internal/twitter_cards.html" . -}} {{ $options := (dict "targetPath" "css/front.css") }} {{ $style := resources.Get "sass/main.scss" | toCSS $options | minify }} {{- if (eq .Section "theories") -}} {{ end }} {{- if or (eq .Section "entries") (eq .File.BaseFileName "search") -}} {{/* The following is the MathJax configuration. This means that formulae can be enclosed in either $ … $ or \( … \) */}} {{ end }} {{- if eq .Section "entries" -}} {{- end -}} - - + {{- if (eq .File.BaseFileName "search") -}} {{- else -}} {{- end -}} + diff --git a/admin/site/themes/afp/layouts/partials/header.html b/admin/site/themes/afp/layouts/partials/header.html --- a/admin/site/themes/afp/layouts/partials/header.html +++ b/admin/site/themes/afp/layouts/partials/header.html @@ -1,38 +1,38 @@
{{ if and (ne .Kind "home") (ne .File.BaseFileName "search") -}} -
+
{{ end -}} {{ .Scratch.Set "title" (default .Site.Title (default .Title .Params.name)) }} {{- if and (eq .Section "authors") (isset .Site.Data.authors (.Scratch.Get "title")) -}} {{- .Scratch.Set "title" (index (index .Site.Data.authors (.Scratch.Get "title")) "name") -}} {{- end -}}

{{ title (.Scratch.Get "title") | replaceRE "[A-Z]" "$0" | safeHTML -}} {{- if (eq .Section "dependencies") }} Dependents{{ end -}}

{{ if (eq .Section "authors") -}} {{ with (index $.Site.Data.authors .Title )}} {{ with .website}}

{{ . }}

{{- end -}}{{- end -}}{{- end -}} {{- $site := . -}} {{ with .Params.authors}}

{{- partial "authors.html" (dict "site" $site "authors" . "affiliations" $site.Params.affiliations) -}} {{ with $site.Params.contributors }} with contributions from {{ partial "authors.html" (dict "site" $site "authors" . "affiliations" $site.Params.affiliations) -}} {{ end }}

{{ end }} {{ with .Params.date }}

{{- dateFormat "January 2, 2006" . -}}

{{ end }}
\ No newline at end of file diff --git a/admin/site/themes/afp/layouts/shortcodes/statistics.html b/admin/site/themes/afp/layouts/shortcodes/statistics.html --- a/admin/site/themes/afp/layouts/shortcodes/statistics.html +++ b/admin/site/themes/afp/layouts/shortcodes/statistics.html @@ -1,216 +1,216 @@
{{ len (where .Site.RegularPages "Section" "==" "entries") }} Entries
{{ len $.Site.Taxonomies.authors }} Authors
~{{ lang.NumFmt 0 (mul (math.Round (div .Site.Data.statistics.num_lemmas 100)) 100) }} Lemmas
~{{ lang.NumFmt 0 (mul (math.Round (div .Site.Data.statistics.num_loc 100)) 100) }} Lines of Code

Most used AFP articles:

{{ range $index, $element := first 12 .Site.Taxonomies.dependencies.ByCount }} - - + + {{ end }}
Name Used by ? articles
{{ add $index 1}}.{{ $element.Page.Title }}{{ $element.Count }}{{ $element.Page.Title }}{{ $element.Count }}
{{- $Scratch := newScratch -}} {{- range ((where site.RegularPages "Section" "entries").GroupByDate "2006" ).Reverse -}} {{- $collection := . -}} {{- $Scratch.Add "years" (slice .Key) -}} {{- with $Scratch.Get "articles_year" -}} {{- $lastYearArticleCount := index (last 1 .) 0 -}} {{- $articleCount := len $collection.Pages -}} {{- $Scratch.Add "articles_year" (slice (int (add $articleCount $lastYearArticleCount))) -}} {{- else }} {{- $Scratch.Add "articles_year" (slice (len .Pages)) -}} {{- end }} {{- end }} {{- range (where site.RegularPages "Section" "entries").Reverse -}} {{- $Scratch.Add "all_articles" (slice (printf "'%s'" .File.BaseFileName )) -}} {{- end }}

Growth in number of articles:

Growth in lines of code:

Growth in number of authors:

Size of articles:

\ No newline at end of file diff --git a/admin/site/themes/afp/layouts/topics/terms.html b/admin/site/themes/afp/layouts/topics/terms.html --- a/admin/site/themes/afp/layouts/topics/terms.html +++ b/admin/site/themes/afp/layouts/topics/terms.html @@ -1,42 +1,42 @@ {{ define "main" }} {{ $topics := .Site.Taxonomies.topics }} {{ range $firstLevel, $secondLevelTaxonomy := .Site.Data.topics }}

{{ $firstLevel }}

{{ with (index $topics (urlize $firstLevel)) }}
{{ range $key := .Pages.ByDate }} - {{ .File.BaseFileName }}   + {{ .File.BaseFileName }}   {{ end }}
{{ end }} {{ with $secondLevelTaxonomy }} {{ range $secondLevel, $thirdLevelTaxonomy := . }}

{{ $secondLevel }}

{{ with (index $topics (printf "%s/%s" (urlize $firstLevel) (urlize $secondLevel))) }} {{ range $key := .Pages.ByDate }} - {{ .File.BaseFileName }}   + {{ .File.BaseFileName }}   {{ end }} {{ end }} {{ with $thirdLevelTaxonomy }} {{ range $thirdLevel, $ignore := . }} {{ end }}
{{ $thirdLevel }} {{ with (index $topics (printf "%s/%s/%s" (urlize $firstLevel) (urlize $secondLevel) (urlize $thirdLevel))) }} {{ range $key := uniq .Pages.ByDate }} - {{ .File.BaseFileName }}   + {{ .File.BaseFileName }}   {{ end }} {{ end }}
{{ end }}
{{ end }} {{ end }} {{ end }} {{ end }} \ No newline at end of file diff --git a/admin/site/themes/afp/static/js/banner.js b/admin/site/themes/afp/static/js/banner.js deleted file mode 100644 --- a/admin/site/themes/afp/static/js/banner.js +++ /dev/null @@ -1,33 +0,0 @@ -document.addEventListener("DOMContentLoaded", () => { - if (localStorageTest() === true) { - const banner = document.getElementById("banner"); - if (banner) { - const bannerID = banner.getAttribute("data-id"); - if (localStorage.getItem("banner-" + bannerID) === "true") { - banner.style = "display: none"; - } - - const close = document.getElementById("close"); - if (close) { - // show the close button if we have JS and local storage access - close.style = ""; - - close.addEventListener("click", () => { - banner.style = "display: none"; - localStorage.setItem("banner-" + bannerID, "true"); - }); - } - } - } -}); - -function localStorageTest() { - if (typeof localStorage !== "undefined") { - localStorage.setItem("test", "yes"); - if (localStorage.getItem("test") === "yes") { - localStorage.removeItem("test"); - return true; - } - } - return false; -} diff --git a/admin/site/themes/afp/static/js/entries.js b/admin/site/themes/afp/static/js/entries.js --- a/admin/site/themes/afp/static/js/entries.js +++ b/admin/site/themes/afp/static/js/entries.js @@ -1,13 +1,13 @@ -document.addEventListener("DOMContentLoaded", function () { - const content = document.getElementById("copyText").innerHTML; - const filename = document.getElementById("bibtexFileName").innerHTML; - document.getElementById("copyBibtex").addEventListener("click", () => { - navigator.clipboard.writeText(content); - }); - - const a = document.getElementById("downloadBibtex"); - var blob = new Blob([content], { type: "text/plain" }); - var url = URL.createObjectURL(blob); - a.setAttribute("href", url); - a.setAttribute("download", filename + ".bib"); -}); +document.addEventListener("DOMContentLoaded", function () { + const content = document.getElementById("copyText").innerHTML + const filename = document.getElementById("bibtexFileName").innerHTML + document.getElementById("copyBibtex").addEventListener("click", () => { + navigator.clipboard.writeText(content) + }) + + const a = document.getElementById("downloadBibtex") + const blob = new Blob([content], {type: "text/plain"}) + const url = URL.createObjectURL(blob) + a.setAttribute("href", url) + a.setAttribute("download", filename + ".bib") +}) diff --git a/admin/site/themes/afp/static/js/flexsearch.min.js b/admin/site/themes/afp/static/js/flexsearch.bundle.js rename from admin/site/themes/afp/static/js/flexsearch.min.js rename to admin/site/themes/afp/static/js/flexsearch.bundle.js --- a/admin/site/themes/afp/static/js/flexsearch.min.js +++ b/admin/site/themes/afp/static/js/flexsearch.bundle.js @@ -1,42 +1,33 @@ -/* - FlexSearch v0.6.30 - Copyright 2019 Nextapps GmbH - Author: Thomas Wilkerling - Released under the Apache 2.0 Licence - https://github.com/nextapps-de/flexsearch -*/ -'use strict';(function(K,R,w){let L;(L=w.define)&&L.amd?L([],function(){return R}):(L=w.modules)?L[K.toLowerCase()]=R:"object"===typeof exports?module.exports=R:w[K]=R})("FlexSearch",function ma(K){function w(a,c){const b=c?c.id:a&&a.id;this.id=b||0===b?b:na++;this.init(a,c);fa(this,"index",function(){return this.a?Object.keys(this.a.index[this.a.keys[0]].c):Object.keys(this.c)});fa(this,"length",function(){return this.index.length})}function L(a,c,b,d){this.u!==this.g&&(this.o=this.o.concat(b),this.u++, -d&&this.o.length>=d&&(this.u=this.g),this.u===this.g&&(this.cache&&this.j.set(c,this.o),this.F&&this.F(this.o)));return this}function S(a){const c=B();for(const b in a)if(a.hasOwnProperty(b)){const d=a[b];F(d)?c[b]=d.slice(0):G(d)?c[b]=S(d):c[b]=d}return c}function W(a,c){const b=a.length,d=O(c),e=[];for(let f=0,h=0;f=h&&(a=a[g-(e+.5>>0)],a=a[b]||(a[b]=[]), -a[a.length]=d);return e}function ba(a,c){if(a){const b=Object.keys(a);for(let d=0,e=b.length;da?1:a?-1:0}function pa(a,c){a=a[M];c=c[M];return ac?1:0}function oa(a,c){const b=M.length;for(let d=0;dc?1:0}function T(a,c,b){return a?{page:a,next:c?""+c:null,result:b}:b}function ha(a,c,b,d,e,f,h){let g,k=[];if(!0===b){b="0";var l=""}else l=b&&b.split(":");const p=a.length;if(1h&&(l=0),l=l||0,g=l+c,g=this.m.length&&(this.C=0),this.m[this.C].postMessage({add:!0,id:a, -content:c}),this.c[f]=""+this.C,b&&b(),this;if(!e){if(this.async&&"function"!==typeof importScripts){let t=this;f=new Promise(function(v){setTimeout(function(){t.add(a,c,null,d,!0);t=null;v()})});if(b)f.then(b);else return f;return this}if(b)return this.add(a,c,null,d,!0),b(),this}c=this.encode(c);if(!c.length)return this;b=this.f;e=O(b)?b(c):c.split(this.split);this.filter&&(e=W(e,this.filter));const n=B();n._ctx=B();const m=e.length,u=this.threshold,q=this.depth,A=this.b,z=this.i,y=this.D;for(let t= -0;tp;x--)l=h.substring(p,x),V(z,n,l,a,v,k,u,A-1)}break;default:if(g=V(z,n,h,a,1,k,u,A-1),q&&1=u)for(g=n._ctx[h]||(n._ctx[h]=B()),h=this.h[h]||(this.h[h]=ia(A-(u||0))),k=t-q,l=t+q+1,0>k&&(k=0),l> -m&&(l=m);kh;d--)e=g[d-1],g[d]=e,f[e]=d;g[h]=c;f[c]=h}}}return b};return a}();return w}(function(){const K={},R="undefined"!==typeof Blob&& -"undefined"!==typeof URL&&URL.createObjectURL;return function(w,L,S,W,P){S=R?URL.createObjectURL(new Blob(["("+S.toString()+")()"],{type:"text/javascript"})):w+".min.js";w+="-"+L;K[w]||(K[w]=[]);K[w][P]=new Worker(S);K[w][P].onmessage=W;return K[w][P]}}()),this); +/**! + * FlexSearch.js v0.7.2 (Bundle) + * Copyright 2018-2021 Nextapps GmbH + * Author: Thomas Wilkerling + * Licence: Apache-2.0 + * https://github.com/nextapps-de/flexsearch + */ +(function _f(self){'use strict';try{if(module)self=module}catch(e){}self._factory=_f;var t;function u(a){return"undefined"!==typeof a?a:!0}function aa(a){const b=Array(a);for(let c=0;c=this.B&&(w||!n[l])){var f=L(q,d,r),g="";switch(this.G){case "full":if(3f;h--)if(h-f>=this.B){var k=L(q,d,r,e,f);g=l.substring(f,h);M(this,n,g,k,a,c)}break}case "reverse":if(2=this.B&&M(this,n, + g,L(q,d,r,e,h),a,c);g=""}case "forward":if(1=this.B&&M(this,n,g,f,a,c);break}default:if(this.C&&(f=Math.min(f/this.C(b,l,r)|0,q-1)),M(this,n,l,f,a,c),w&&1=this.B&&!e[l]){e[l]=1;const p=this.l&&l>f;M(this,m,p?f:l,L(g+(d/2>g?0:1),d,r,h-1,k-1),a,c,p?l:f)}}}}this.m||(this.register[a]=1)}}return this}; + function L(a,b,c,d,e){return c&&1=this.B&&!c[q])if(this.s||f||this.map[q])k[w++]=q,c[q]=1;else return d;a=k;e=a.length}if(!e)return d;b||(b=100);h=this.depth&&1=d)))break;if(n){if(f)return ta(k,d,0);b[b.length]=k;return}}return!c&&k}function ta(a,b,c){a=1===a.length?a[0]:[].concat.apply([],a);return c||a.length>b?a.slice(c,c+b):a} + function ua(a,b,c,d){c?(d=d&&b>c,a=(a=a[d?b:c])&&a[d?c:b]):a=a[b];return a}t.contain=function(a){return!!this.register[a]};t.update=function(a,b){return this.remove(a).add(a,b)}; + t.remove=function(a,b){const c=this.register[a];if(c){if(this.m)for(let d=0,e;db||c)e=e.slice(c,c+b);d&&(e=za.call(this,e));return{tag:a,result:e}}}function za(a){const b=Array(a.length);for(let c=0,d;c 1) { - executeSearch(indices, this.value); - } - } - }); - - - input.addEventListener("keydown", function (event) { - switch (event.key) { - case "Enter": - event.preventDefault(); // prevent the form from being submitted - handleSubmit(this.value); - break; - default: - } - }); - - input.addEventListener("change", function () { - handleSubmit(this.value); - }); -} - -function executeSearch(indices, searchQuery) { - var suggestResults = indices["suggest"].search({ - query: searchQuery, - limit: 10, - }); - - if (!(suggestResults.length === 1 && suggestResults[0].keyword === searchQuery)) { - filterAutocomplete(suggestResults); - } else { - filterAutocomplete(); - } -} - -function handleSubmit(value) { - if (typeof history.pushState !== "undefined") { - document.location = window.location.origin + "/search/?s=" + value; - } else { - var url = "TODO"; - window.location.assign(url); - } -} - -// Autocomplete ------------------------------------------------------------------------ - -function filterAutocomplete(values) { - const list = document.getElementById("autocomplete"); - if (list) { - if (values) { - let i = 0; - for (let value of values) { - let elem = document.createElement("option"); - elem.value = value.keyword; - if (i < list.childNodes.length) { - list.childNodes[i].replaceWith(elem); - i++; - } else { - list.appendChild(elem); - } - } - if (values.length < list.childNodes.length) { - for (let j = 0; j < list.childNodes.length - values.length; j++) { - list.removeChild(list.lastChild); - } - } - } else { - while (list.firstChild) { - list.removeChild(list.lastChild); - } - } - } -} - -document.addEventListener("DOMContentLoaded", function () { - var input = document.getElementById("searchInput"); - var button = document.getElementById("searchButton"); - if (button) { - button.addEventListener("click", () => { - handleSubmit(input.value); - }); - } - - Promise.all([fetch("/data/keywords.json")]) - .then(function (responses) { - // Get a JSON object from each of the responses - return Promise.all(responses.map((response) => response.json())); - }) - .then((data) => loadSearch(input, ...data)); -}); +function load_search(input, keywords) { + const suggest_index = get_suggest_index(keywords) + + input.addEventListener("keyup", function (event) { + switch (event.key) { + case "Enter": + case "Up": + case "ArrowUp": + case "Down": + case "ArrowDown": + case "Left": + case "ArrowLeft": + case "Right": + case "ArrowRight": + case "Escape": + break + default: + if (this.value && this.value.length > 1) { + add_suggestions(suggest_index, this.value) + } + } + }) + + input.addEventListener("keydown", function (event) { + switch (event.key) { + case "Enter": + event.preventDefault() // prevent the form from being submitted + handle_submit(this.value) + break + default: + } + }) + + input.addEventListener("change", function () { + handle_submit(this.value) + }) +} + +function handle_submit(value) { + if (typeof history.pushState !== "undefined") { + document.location = window.location.origin + "/search/?s=" + value + } +} + +document.addEventListener("DOMContentLoaded", function () { + const input = document.getElementById("searchInput") + const button = document.getElementById("searchButton") + if (button) { + button.addEventListener("click", () => { + handle_submit(input.value) + }) + } + + Promise.all([fetch("/data/keywords.json")]) + .then(function (responses) { + // Get a JSON object from each of the responses + return Promise.all(responses.map((response) => response.json())) + }) + .then((data) => load_search(input, ...data)) +}) diff --git a/admin/site/themes/afp/static/js/search-autocomplete.js b/admin/site/themes/afp/static/js/search-autocomplete.js new file mode 100644 --- /dev/null +++ b/admin/site/themes/afp/static/js/search-autocomplete.js @@ -0,0 +1,57 @@ +/* constants */ + +const ID_AUTOCOMPLETE = "autocomplete" + +const get_suggest_index = (keywords) => +{ + const index = new FlexSearch.Document({ + encoder: "icase", + tokenize: "forward", + document: { + index: "keyword", + store: true, + } + }); + keywords.forEach(keyword => index.add(keyword)) + return index +} + +const add_suggestions = (index, query) => +{ + const suggest_results = index.search(query, { pluck: 'keyword', enrich: true }).map(d => d.doc) + + if (!(suggest_results.length === 1 && suggest_results[0].keyword === query)) { + filter_autocomplete(suggest_results); + } else { + filter_autocomplete(); + } +} + +function filter_autocomplete(values) +{ + const list = document.getElementById(ID_AUTOCOMPLETE); + if (list) { + if (values) { + let i = 0; + for (let value of values) { + let elem = document.createElement("option"); + elem.value = value.keyword; + if (i < list.childNodes.length) { + list.childNodes[i].replaceWith(elem); + i++; + } else { + list.appendChild(elem); + } + } + if (values.length < list.childNodes.length) { + for (let j = 0; j < list.childNodes.length - values.length; j++) { + list.removeChild(list.lastChild); + } + } + } else { + while (list.firstChild) { + list.removeChild(list.lastChild); + } + } + } +} diff --git a/admin/site/themes/afp/static/js/search.js b/admin/site/themes/afp/static/js/search.js --- a/admin/site/themes/afp/static/js/search.js +++ b/admin/site/themes/afp/static/js/search.js @@ -1,423 +1,302 @@ -function loadSearch(entries, authors, topics, keywords) { - var entryIndex = new FlexSearch({ - encode: "advanced", - tokenize: "forward", - bool: "or", - doc: { - id: "id", - field: ["title", "abstract", "date", "authors"], - }, - }); - - var authorIndex = new FlexSearch({ - encode: "advanced", - tokenize: "forward", - doc: { - id: "id", - field: "name", - }, - }); - - var topicIndex = new FlexSearch({ - encode: "icase", - tokenize: "forward", - doc: { - id: "id", - field: "name", - }, - }); - - var suggestIndex = new FlexSearch({ - encode: "icase", - tokenize: "forward", - doc: { - id: "id", - field: "keyword", - }, - }); - - var indices = { - entry: entryIndex, - author: authorIndex, - topic: topicIndex, - suggest: suggestIndex, - }; - - indices["entry"].add(entries); - indices["author"].add(authors); - indices["topic"].add(topics); - indices["suggest"].add(keywords); - - var memoQueryFindFacts = memoizer(queryFindFacts); - const input = document.getElementById("searchInput"); - - var searchTerm = input.value; - if (searchTerm) { - executeSearch(indices, searchTerm); - memoQueryFindFacts(searchTerm).then((results) => - populateFindFactsResults(searchTerm, results) - ); - } - - input.addEventListener("keyup", function (event) { - switch (event.key) { - case "Enter": - case "Up": - case "ArrowUp": - case "Down": - case "ArrowDown": - case "Left": - case "ArrowLeft": - case "Right": - case "ArrowRight": - case "Escape": - break; - default: - if (this.value && this.value.length > 1) { - executeSearch(indices, this.value); - } else { - clearResults(); - } - } - }); - - input.addEventListener("keyup", debounce(() => { - var searchTerm = input.value; - if (searchTerm && searchTerm.length > 2) { - memoQueryFindFacts(searchTerm).then((results) => - populateFindFactsResults(searchTerm, results) - ); - } - }, 300)); - - input.addEventListener("keydown", function (event) { - switch (event.key) { - case "Enter": - event.preventDefault(); // prevent the form from being submitted - handleSubmit(this.value); - break; - default: - } - }); - - async function queryFindFacts(searchTerm) { - var body = '{"filters":[{"field":"SourceCode","filter":{"Term":{"inner":"'; - body += searchTerm + '"}}}],'; - body += '"fields":["Command","ConstantTypeFacet","Kind","SourceTheoryFacet"],'; - body += '"maxFacets":5}'; - - const response = await fetch( - "https://search.isabelle.in.tum.de/v1/default_Isabelle2021_AFP2021/facet", - { - method: "POST", - headers: { - "Content-Type": "application/json", - accept: "application/json", - }, - body: body, - } - ); - const data = await response.json(); - return data["Kind"]; - } - - function debounce(callback, wait) { - let timeout; - return (...args) => { - clearTimeout(timeout); - timeout = setTimeout(function () { - callback.apply(this, args); - }, wait); - }; - } - - function memoizer(fun) { - let cache = {}; - return function (n) { - if (cache[n] != undefined) { - return cache[n]; - } else { - let result = fun(n); - cache[n] = result; - return result; - } - }; - } -} - -function executeSearch(indices, searchQuery) { - var entryResults = indices["entry"].search({ - query: searchQuery, - limit: 16, - }); - - var topicResults = indices["topic"].search({ - query: searchQuery, - limit: 5, - }); - - var authorResults = indices["author"].search({ - query: searchQuery, - limit: 5, - }); - - var suggestResults = indices["suggest"].search({ - query: searchQuery, - limit: 10, - }); - - if (entryResults.length > 0) { - populateResults(entryResults, searchQuery, indices); - } else { - setInnerHTMLOfID("search-results", "

No results

"); - } - - if (authorResults.length > 0) { - populateSmallResults(authorResults, searchQuery, "author", indices); - } else { - setInnerHTMLOfID("author-results", "

No results

"); - } - - if (topicResults.length > 0) { - populateSmallResults(topicResults, searchQuery, "topic", indices); - } else { - setInnerHTMLOfID("topic-results", "

No results

"); - } - - if (!(suggestResults.length === 1 && suggestResults[0].keyword === searchQuery)) { - filterAutocomplete(suggestResults); - } else { - filterAutocomplete(); - } -} - -function populateResults(results, searchQuery, indices, all = false) { - if (searchQuery.length < 3) { - setInnerHTMLOfID("find-facts-results", ""); - } else { - setInnerHTMLOfID("find-facts-results", "..."); - } - - const resultsTable = document.getElementById("search-results"); - - setInnerHTMLOfID("search-results", ""); - - var limit = all ? results.length : 15; - - results.slice(0, limit).forEach(function (result, resultKey) { - var topics = []; - - result.topics.forEach((value, key) => { - topics[key] = "" + value + ""; - }); - - var topicString = niceList(topics); - var authorString = niceList(result.authors); - - var title = result.title; - var link = result.shortname.toLowerCase(); - var shortname = result.shortname; - var abstract = result.abstract; - var used_by = result.used_by; - var year = result.date.substring(0, 4); - - var output = `
-
- ${title} - Download -
-
- ${authorString ? `

${authorString}

` : ""} - ${year ? `

${year}

` : ""} -
-
${abstract}
- ${ used_by - ? `
Used by ${used_by} | ${ - topicString ? `${topicString} ` : "" - }
` - : topicString ? `
${topicString}
` : "" - } -
`; - - resultsTable.insertAdjacentHTML("beforeend", output); - }); - - if (results.length > 15 && !all) { - var btn = document.createElement("button"); - btn.innerHTML = "Show all results"; - - btn.addEventListener("click", function () { - var entryResults = indices["entry"].search({ - query: searchQuery, - }); - - populateResults(entryResults, searchQuery, indices, true); - }); - - resultsTable.appendChild(btn); - } - - new Mark(resultsTable).mark(searchQuery); - - function niceList(topics) { - if (topics.length <= 2) { - topicString = topics.join(" and "); - } else { - topicString = - topics.slice(0, -1).join(", ") + " and " + topics[topics.length - 1]; - } - return topicString; - } -} - -function clearResults() { - setInnerHTMLOfID("author-results", ""); - setInnerHTMLOfID("topic-results", ""); - setInnerHTMLOfID("find-facts-results", ""); - setInnerHTMLOfID("search-results", "

Please enter a search term above

"); -} - -function populateSmallResults(results, searchQuery, key, indices, all = false) { - const maxResults = 4; - setInnerHTMLOfID(key + "-results", ""); - - var resultsTable = document.getElementById(key + "-results"); - - var limit = all ? results.length : maxResults; - var list = document.createElement("ul"); - - results.slice(0, limit).forEach((result, resultKey) => { - var listElement = document.createElement("li"); - var anchor = document.createElement("a"); - anchor.href = result.link; - anchor.innerHTML = result.name; - listElement.appendChild(anchor); - list.appendChild(listElement); - }); - - resultsTable.insertAdjacentElement("beforeend", list); - - if (results.length > maxResults && !all) { - const btn = document.createElement("button"); - btn.innerHTML = "Show all"; - - btn.addEventListener("click", function () { - var entryResults = indices[key].search({ - query: searchQuery, - }); - - populateSmallResults(entryResults, searchQuery, key, indices, true); - }); - - resultsTable.insertAdjacentElement("beforeend", btn); - } - - new Mark(resultsTable).mark(searchQuery); -} - -function populateFindFactsResults(searchTerm, data) { - var resultsElement = document.getElementById("find-facts-results"); - if (Object.keys(data).length !== 0 && resultsElement) { - let urlPrefix = - 'https://search.isabelle.in.tum.de/#search/default_Isabelle2021_AFP2021?q={"term":"'; - urlPrefix += searchTerm + '","facets":{"Kind":["'; - const urlSuffix = '"]}}'; - - var list = document.createElement("ul"); - - Object.entries(data).forEach(([name, count]) => { - var listElement = document.createElement("li"); - var anchor = document.createElement("a"); - anchor.href = urlPrefix + name + urlSuffix; - anchor.target = "_blank"; - anchor.rel = "noreferrer noopener"; - anchor.innerHTML = count + " " + name + "s"; - listElement.appendChild(anchor); - list.appendChild(listElement); - }); - - setInnerHTMLOfID("find-facts-results", ""); - resultsElement.insertAdjacentElement("beforeend", list); - } else { - setInnerHTMLOfID("find-facts-results", "

No results

"); - } -} - -function handleSubmit(value) { - if (typeof history.pushState !== "undefined") { - history.pushState({}, "Search the Archive - " + value, "?s=" + value); - } else { - var url = "TODO"; - window.location.assign(url); - } -} - -// Autocomplete ------------------------------------------------------------------------ - -function filterAutocomplete(values) { - const list = document.getElementById("autocomplete"); - if (list) { - if (values) { - let i = 0; - for (let value of values) { - let elem = document.createElement("option"); - elem.value = value.keyword; - if (i < list.childNodes.length) { - list.childNodes[i].replaceWith(elem); - i++; - } else { - list.appendChild(elem); - } - } - if (values.length < list.childNodes.length) { - for (let j = 0; j < list.childNodes.length - values.length; j++) { - list.removeChild(list.lastChild); - } - } - } else { - while (list.firstChild) { - list.removeChild(list.lastChild); - } - } - } -} - -function setInnerHTMLOfID(id, str) { - const elem = document.getElementById(id); - if (elem) { - elem.innerHTML = str; - } else { - console.log("Failed to find:", id, "for innerHTML. Would have set it to", str); - } -} - -document.addEventListener("DOMContentLoaded", function () { - var input = document.getElementById("searchInput"); - var urlQuery = param("s"); - if (urlQuery) { - input.value = urlQuery; - } - input.focus(); - - document.getElementById("searchButton").addEventListener("click", () => { - handleSubmit(document.getElementById("searchInput").value); - }); - - Promise.all([ - fetch("/index.json"), - fetch("/authors/index.json"), - fetch("/topics/index.json"), - fetch("/data/keywords.json"), - ]) - .then(function (responses) { - // Get a JSON object from each of the responses - return Promise.all(responses.map((response) => response.json())); - }) - .then((data) => loadSearch(...data)); - - function param(name) { - return decodeURIComponent( - (location.search.split(name + "=")[1] || "").split("&")[0] - ).replace(/\+/g, " "); - } -}); +/* constants */ + +const URL_FINDFACTS = 'https://search.isabelle.in.tum.de' + +const NUM_MAX_SIDE_RESULTS = 4 +const NUM_MAX_MAIN_RESULTS = 15 + +const ID_SEARCH_INPUT = 'searchInput' +const ID_SEARCH_BUTTON = 'searchButton' +const ID_RESULTS_ENTRIES = 'search-results' +const ID_RESULTS_AUTHORS = 'author-results' +const ID_RESULTS_TOPICS = 'topic-results' +const ID_RESULTS_FINDFACTS = 'find-facts-results' + + +/* index */ + +function build_indexes(entries, authors, topics, keywords) { + const entry_index = new FlexSearch.Document({ + encoder: 'advanced', + tokenize: 'forward', + document: { + id: 'id', + index: ['title', 'abstract', 'date', 'topics[]', 'authors[]'], + store: true, + }, + }) + entries.forEach(entry => entry_index.add(entry)) + + const author_index = new FlexSearch.Document({ + encoder: 'advanced', + tokenize: 'forward', + document: { + id: 'id', + index: 'name', + store: true + }, + }) + authors.forEach(author => author_index.add(author)) + + const topic_index = new FlexSearch.Document({ + encoder: 'icase', + tokenize: 'forward', + document: { + id: 'id', + index: 'name', + store: true + }, + }) + topics.forEach(topic => topic_index.add(topic)) + + const suggest_index = get_suggest_index(keywords) + + return { + entry: entry_index, + author: author_index, + topic: topic_index, + suggest: suggest_index, + } +} + +async function get_findfacts_index() { + const indexes = await fetch(URL_FINDFACTS + '/v1/indexes').then(async http_res => { + if (http_res.status !== 200) { + console.log(`Error ${http_res.status} when fetching indexes: ${http_res.statusText}`) + return Promise.resolve([]) + } + return await http_res.json() + }).catch((err) => { + console.log(`Could not fetch indexes: ${err}`) + return Promise.resolve([]) + }) + + return indexes.find(index => index.startsWith('default_')) +} + + +/* search */ + +function local_search(indices, query) { + const entry_results = [...new Set(indices['entry'].search(query, NUM_MAX_MAIN_RESULTS + 1, + {enrich: true}).flatMap(e => e.result).map(d => d.doc))] + const topic_results = indices['topic'].search(query, NUM_MAX_SIDE_RESULTS + 1, + {enrich: true, pluck: 'name'}).map(d => d.doc) + const author_results = indices['author'].search(query, NUM_MAX_SIDE_RESULTS + 1, + {enrich: true, pluck: 'name'}).map(d => d.doc) + return {entries: entry_results, topics: topic_results, authors: author_results} +} + +async function findfacts_search(index, query) { + if (!index) return {} + const facet_query = { + filters: [ + { + field: 'SourceCode', + filter: { + Term: { + inner: query + } + } + } + ], + fields: ['Kind'], + maxFacets: 5 + } + const facet = await fetch(`${URL_FINDFACTS}/v1/${index}/facet`, { + method: 'POST', + mode: 'cors', + headers: { + 'Content-Type': 'application/json', + }, + body: JSON.stringify(facet_query), + } + ).then(async (response) => { + if (response.status !== 200) { + console.log(`Error ${http_res.status} on findfacts query: ${http_res.statusText}`) + return {} + } else { + const json = await response.json() + return json['Kind'] + } + }).catch((err) => { + console.log(`Error in findfacts query: ${err}`) + return {} + }) + const search_query = `{"term"%3A"${encodeURIComponent(query)}"}` + const url = `${URL_FINDFACTS}/#search/${index}?q=${search_query}` + + return {facet: facet, url: url} +} + + +/* result handling */ + +function render_entry(entry) { + const authors = entry.authors.join(', ') + const topics = entry.topics.map((topic, key) => + `${topic}`).join(', ') + const year = entry.date.substring(0, 4) + + return ` +
+
+

+ ${entry.title} +

+
+
+ ${authors} + ${year} +
+
${entry.abstract}
+
in ${topics}
+
` +} + +function render_entries_results(data, query) { + if (!data) return parse_elem('

Please enter a search term above.

') + if (data.length === 0) return parse_elem('

No results.

') + else { + const end = data.length > NUM_MAX_MAIN_RESULTS ? '...' : '' + const res = parse_elem(` + ${data.slice(0, NUM_MAX_MAIN_RESULTS).map(entry => render_entry(entry)).join('')}${end}`) + new Mark(res).mark(query) + return res + } +} + +function render_results_shortlist(data, query) { + if (!data) return '' + if (data.length === 0) return parse_elem('

No results

') + else { + const end = data.length > NUM_MAX_SIDE_RESULTS ? '
  • ...
    • ' : '' + const res = parse_elem(` +
      ${data.slice(0, NUM_MAX_SIDE_RESULTS).map(item => ` +
    • + ${item.name} +
      • `).join('')} + ${end} +
    `) + new Mark(res).mark(query) + return res + } +} + +function render_findfacts_results(res) { + if (res.facet && Object.keys(res.facet).length > 0) { + return parse_elem(` + `) + } else return parse_elem('

    No results

    ') +} + + +/* input handling */ + +function debounce(callback, wait) { + let timeout + return (...args) => { + clearTimeout(timeout) + timeout = setTimeout(function () { + callback.apply(this, args) + }, wait) + } +} + +function handleSubmit(value) { + if (typeof history.pushState !== 'undefined') { + history.pushState({}, 'Search the Archive - ' + value, '?s=' + value) + } +} + + +/* setup */ + +const init_search = async () => { + const input = document.getElementById(ID_SEARCH_INPUT) + const button = document.getElementById(ID_SEARCH_BUTTON) + const entries_res = document.getElementById(ID_RESULTS_ENTRIES) + const authors_res = document.getElementById(ID_RESULTS_AUTHORS) + const topics_res = document.getElementById(ID_RESULTS_TOPICS) + + const search_query = get_query('s') + if (search_query) input.value = search_query.replace('+', ' ') + + const index_data = await Promise.all([ + fetch('/index.json'), + fetch('/authors/index.json'), + fetch('/topics/index.json'), + fetch('/data/keywords.json') + ]) + const index_json = await Promise.all(index_data.map(r => r.json())) + const indexes = build_indexes(...index_json) + + input.addEventListener('keydown', (event) => { + switch (event.key) { + case 'Enter': + event.preventDefault() + handleSubmit(event.target.value) + } + }) + + const run_local_search = (query) => { + let res = {} + if (query && query.length > 1) { + add_suggestions(indexes['suggest'], query) + res = local_search(indexes, query) + } + authors_res.replaceChildren(render_results_shortlist(res.authors, query)) + topics_res.replaceChildren(render_results_shortlist(res.topics, query)) + entries_res.replaceChildren(render_entries_results(res.entries, query)) + MathJax.typeset() + } + + input.addEventListener('keyup', (event) => { + switch (event.key) { + case 'Enter': + case 'Up': + case 'ArrowUp': + case 'Down': + case 'ArrowDown': + case 'Left': + case 'ArrowLeft': + case 'Right': + case 'ArrowRight': + case 'Escape': + break + default: + run_local_search(event.target.value) + } + }) + button.addEventListener('click', () => handleSubmit(input.value)) + + if (input.value) run_local_search(input.value) + input.focus() + + // findfacts + const findfacts_res = document.getElementById(ID_RESULTS_FINDFACTS) + const findfacts_index = await get_findfacts_index() + const memoized_findfacts_search = memoize(findfacts_search) + + const run_findfacts_search = async (query) => { + let res = {} + if (query && query.length > 2) { + findfacts_res.replaceChildren(parse_elem('

    ...

    ')) + res = await memoized_findfacts_search([findfacts_index, query]) + } + findfacts_res.replaceChildren(render_findfacts_results(res)) + } + + input.addEventListener('keyup', debounce(async (event) => + run_findfacts_search(event.target.value), 300)) + + if (input.value) await run_findfacts_search(input.value) +} + +document.addEventListener('DOMContentLoaded', init_search) diff --git a/admin/site/themes/afp/static/js/theory.js b/admin/site/themes/afp/static/js/theory.js --- a/admin/site/themes/afp/static/js/theory.js +++ b/admin/site/themes/afp/static/js/theory.js @@ -1,294 +1,277 @@ /* constants */ const ID_THEORY_LIST = 'theories' const CLASS_LOADER = 'loader' const CLASS_ANIMATION = 'animation' const ATTRIBUTE_THEORY_SRC = 'theory-src' const CLASS_NAVBAR_TYPE = 'theory-navbar-type' const CLASS_THY_NAV = 'thy-nav' const PARAM_NAVBAR_TYPE = 'theory-navbar-type' const ID_NAVBAR_TYPE_SELECTOR = 'navbar-type-selector' const ID_NAVBAR = 'theory-navbar' const NAVBAR_TYPES = ['fact', 'type', 'const'] /* routing */ function target(base_href, rel_href) { const href_parts = rel_href.split('/') if (href_parts.length === 1) return `#${href_parts[0]}` else if (href_parts.length === 3 && href_parts[0] === '..' && href_parts[1] !== '..') { return `/entries/${href_parts[1].toLowerCase()}/theories#${href_parts[2]}` } else return `${base_href}/${rel_href}` } function to_id(thy_name, ref) { if (ref) return `${thy_name}.html#${ref}` else return `${thy_name}.html` } const to_svg_id = (thy_name) => `${thy_name}#svg` const to_container_id = (thy_name) => `${thy_name}#container` const to_collapsible_id = (thy_name) => `${thy_name}#collapsible` const to_spinner_id = (thy_name) => `${thy_name}#spinner` const to_nav_id = (thy_name) => `${thy_name}#nav` const to_ul_id = (thy_name) => `${thy_name}#ul` const of_ul_id = (id) => id.split('#').slice(0, -1).join('#') const to_a_id = (thy_name) => `${thy_name}#a` -function set_query(attribute, value) { - const params = new URLSearchParams(window.location.search) - params.set(attribute, value) - - const fragment = window.location.hash.length > 1 ? window.location.hash : '' - const new_url = `${window.location.origin}${window.location.pathname}?${params.toString()}${fragment}` - - if (history.pushState) window.history.pushState({ path: new_url }, '', new_url) - else window.location = new_url -} - -function get_query(attribute) { - const params = new URLSearchParams(window.location.search) - return params.get(attribute) -} - - /* document translation */ function translate(base_href, thy_name, thy_body) { const thy_refs = [...thy_body.getElementsByTagName('span')].map((span) => { let ref = span.getAttribute('id') if (ref) { span.setAttribute('id', to_id(thy_name, ref)) } return ref }).filter(e => e) for (const link of thy_body.getElementsByTagName('a')) { const rel_href = link.getAttribute('href') link.setAttribute('href', target(base_href, rel_href)) } return thy_refs } /* theory lazy-loading */ async function fetch_theory_body(href) { const html_str = await fetch(href).then((http_res) => { if (http_res.status !== 200) return Promise.resolve(`${http_res.statusText}`) else return http_res.text() }).catch((_) => { console.log(`Could not load theory at '${href}'. Redirecting...`) window.location.replace(href) }) const parser = new DOMParser() const html = parser.parseFromString(html_str, 'text/html') return html.getElementsByTagName('body')[0] } async function load_theory(thy_name, href) { const thy_body = await fetch_theory_body(href) const refs = translate(href, thy_name, thy_body) const collapse = document.getElementById(to_collapsible_id(thy_name)) collapse.append(...Array(...thy_body.children).slice(1)) return refs } async function open_theory(thy_name) { const container = document.getElementById(to_container_id(thy_name)) if (container) { if (document.getElementById(to_collapsible_id(thy_name))) open(container) else { const collapsible = parse_elem(`
    `) container.appendChild(collapsible) open(container) let refs = await load_theory(thy_name, container.getAttribute(ATTRIBUTE_THEORY_SRC)) await load_theory_nav(thy_name, refs) const spinner = document.getElementById(to_spinner_id(thy_name)) spinner.parentNode.removeChild(spinner) } } } function nav_tree_rec(thy_name, path, key, ref_parts, type) { const rec_ref = ref_parts.filter(e => e.length > 0) const id = to_id(thy_name, `${path.join('.')}.${key}|${type}`) let res if (rec_ref.length < ref_parts.length) { res = `${escape_html(key)}` } else { const head_id = to_id(thy_name, `${[...path, key, ...ref_parts[0]].join('.')}|${type}`) res = `${escape_html(key)}` } if (rec_ref.length > 1) { const by_key = group_by(rec_ref) const children = Object.keys(by_key).map((key1) => `
  • ${nav_tree_rec(thy_name, [...path, key], key1, by_key[key1], type)}
    • `) return ` ${res}
      ${children.join('')}
    ` } else return res } function nav_tree(thy_name, refs, type) { let trees = Object.entries(group_by(refs || [])).map(([key, parts]) => `
  • ${nav_tree_rec(thy_name, [thy_name], key, parts, type)}
    • `) return parse_elem(`
      ${trees.join('')}
    `) } const cached_refs = Object.fromEntries(NAVBAR_TYPES.map(t => [t, {}])) const load_theory_nav = (thy_name, refs) => { let selected = get_query(PARAM_NAVBAR_TYPE) || NAVBAR_TYPES[0] let by_type = group_by(refs.filter(ref => ref.includes('|')).map((id) => id.split('|').reverse())) let type_selector = document.getElementById(ID_NAVBAR_TYPE_SELECTOR) let options = [...type_selector.options].map(e => e.value) for (let [type, elems] of Object.entries(by_type)) { if (NAVBAR_TYPES.includes(type) && !options.includes(type)) { type_selector.appendChild(parse_elem(``)) } let parts_by_thy = group_by(elems.map((s) => s[0].split('.'))) if (NAVBAR_TYPES.includes(type)) cached_refs[type][thy_name] = parts_by_thy[thy_name] } let tree = nav_tree(thy_name, cached_refs[selected][thy_name], selected) document.getElementById(to_nav_id(thy_name)).appendChild(tree) ScrollSpy.instance.refresh() } /* state */ let navbar_last_opened = [] /* controls */ const follow_theory_hash = async () => { let hash = window.location.hash if (hash.length > 1) { const id = hash.slice(1) const thy_name = strip_suffix(id.split('#')[0], '.html') await open_theory(thy_name) const elem = document.getElementById(id) if (elem) elem.scrollIntoView() } } const toggle_theory = async (thy_name) => { const hash = `#${to_id(thy_name)}` const collapsible = document.getElementById(to_container_id(thy_name)) if (collapsible) { if (!collapse(collapsible)) { if (window.location.hash === hash) open(collapsible) else window.location.hash = hash } } else window.location.hash = hash } const change_selector = (type) => { let old_type = get_query(PARAM_NAVBAR_TYPE) if (!old_type || old_type !== type) { set_query(PARAM_NAVBAR_TYPE, type) for (const elem of document.getElementsByClassName(CLASS_NAVBAR_TYPE)) { let thy_name = of_ul_id(elem.id) elem.replaceWith(nav_tree(thy_name, cached_refs[type][thy_name], type)) } ScrollSpy.instance.refresh() } } const open_tree = (elem) => { if (elem.classList.contains(CLASS_COLLAPSIBLE)) { if (open(elem)) navbar_last_opened.push(elem) } if (elem.parentElement) open_tree(elem.parentElement) } const sync_navbar = (link) => { for (const elem of navbar_last_opened){ collapse(elem) } open_tree(link.parentElement) link.scrollIntoView({block: "center"}) } /* setup */ const init = async () => { const theory_list = document.getElementById(ID_THEORY_LIST) const navbar = document.getElementById(ID_NAVBAR) if (theory_list && navbar) { const thy_names = [] for (const theory of theory_list.children) { thy_names.push(theory.id) const href = theory.getAttribute('href') const thy_name = theory.id const thy_collapsible = parse_elem(`

    ${thy_name}

    `) theory.replaceWith(thy_collapsible) } const type = get_query(PARAM_NAVBAR_TYPE) ? get_query(PARAM_NAVBAR_TYPE) : NAVBAR_TYPES[0] navbar.appendChild(parse_elem(`
    • `)) navbar.append(...thy_names.map((thy_name) => parse_elem(`
  • ${thy_name}
    • `)), parse_elem('
    ')) window.onhashchange = follow_theory_hash window.addEventListener(EVENT_SPY_ACTIVATE, (e) => sync_navbar(e.relatedTarget)) new ScrollSpy(document.body, ID_NAVBAR) await follow_theory_hash() } } document.addEventListener('DOMContentLoaded', init) diff --git a/admin/site/themes/afp/static/js/util.js b/admin/site/themes/afp/static/js/util.js --- a/admin/site/themes/afp/static/js/util.js +++ b/admin/site/themes/afp/static/js/util.js @@ -1,68 +1,97 @@ /* utilities */ const CLASS_COLLAPSED = 'collapsed' const CLASS_COLLAPSIBLE = 'collapsible' const CLASS_INVERTIBLE = 'invertible' const CLASS_COLLAPSE_CONTAINER = 'collapse-container' const strip_suffix = (str, suffix) => { if (str.endsWith(suffix)) return str.slice(0, -suffix.length) else return str } const group_by = (elems) => { return elems.reduce((ks, kv) => { if (kv.isEmpty) return ks else { const k = kv[0] const vs = kv.slice(1) if (ks[k]) ks[k].push(vs) else ks[k] = [vs] return ks } }, {}) } const parse_elem = (html_str) => { const template = document.createElement('template') template.innerHTML = html_str return template.content } const is_collapsed = (e) => { return e.classList.contains(CLASS_COLLAPSED) } const open = (collapsible) => { if (collapsible.classList.contains(CLASS_COLLAPSED)) { collapsible.classList.remove(CLASS_COLLAPSED) return true } else return false } const collapse = (collapsible) => { if (!collapsible.classList.contains(CLASS_COLLAPSED)) { collapsible.classList.add(CLASS_COLLAPSED) return true } else return false } const escape_html = (html) => { return html.replace(/[&<>"']/g, function(m) { switch (m) { case '&': return '&' case '<': return '<' case '>': return '>' case '"': return '"' case "'": return ''' } }) -} \ No newline at end of file +} + +function set_query(attribute, value) { + const params = new URLSearchParams(window.location.search) + params.set(attribute, value) + + const fragment = window.location.hash.length > 1 ? window.location.hash : '' + const new_url = `${window.location.origin}${window.location.pathname}?${params.toString()}${fragment}` + + if (history.pushState) window.history.pushState({ path: new_url }, '', new_url) + else window.location = new_url +} + +function get_query(attribute) { + const params = new URLSearchParams(window.location.search) + return params.get(attribute) +} + +function memoize(fun) { + const cache = {} + return function (n) { + if (cache[n] !== undefined) { + return cache[n] + } else { + let result = fun(...n) + cache[n] = result + return result + } + } +} diff --git a/tools/afp_site_gen.scala b/tools/afp_site_gen.scala --- a/tools/afp_site_gen.scala +++ b/tools/afp_site_gen.scala @@ -1,265 +1,265 @@ package afp import isabelle._ object AFP_Site_Gen { /* json */ object JSON { type T = isabelle.JSON.T object Object { type T = isabelle.JSON.Object.T } def from_authors(authors: List[Metadata.Author]): T = Metadata.TOML.from_authors(authors) def from_topics(topics: List[Metadata.Topic]): T = Metadata.TOML.from_topics(topics) def from_affiliations(affiliations: List[Metadata.Affiliation]): Object.T = { Utils.group_sorted(affiliations, (a: Metadata.Affiliation) => a.author).view.mapValues(author_affiliations => { val homepage = author_affiliations.collectFirst { case Metadata.Homepage(_, _, url) => url } val email = author_affiliations.collectFirst { case Metadata.Email(_, _, address) => address } isabelle.JSON.Object( homepage.map(s => List("homepage" -> s)).getOrElse(Nil) ::: email.map(s => List("email" -> s)).getOrElse(Nil): _*) }).toMap } def from_change_history(history: Metadata.Change_History): Object.T = { if (history.isEmpty) { Map.empty } else { Map("Change history" -> history.map { case (date, str) => "[" + date.toString + "] " + str }.mkString("\n")) } } def from_entry(entry: Metadata.Entry): JSON.Object.T = isabelle.JSON.Object( "title" -> entry.title :: "authors" -> entry.authors.map(_.author).distinct :: "affiliations" -> from_affiliations(entry.authors ++ entry.contributors) :: (if (entry.contributors.nonEmpty) "contributors" -> entry.contributors.map(_.author).distinct :: Nil else Nil) ::: "date" -> entry.date.toString :: "topics" -> entry.topics.map(_.id) :: "abstract" -> entry.`abstract` :: "license" -> entry.license :: (if (entry.releases.nonEmpty) "releases" -> entry.releases.map(r => r.isabelle -> r.date.toString).toMap :: Nil else Nil) ::: (if (entry.note.nonEmpty) "note" -> entry.note :: Nil else Nil) ::: (if (entry.change_history.nonEmpty || entry.extra.nonEmpty) "extra" -> (from_change_history(entry.change_history) ++ entry.extra) :: Nil else Nil): _*) def from_keywords(keywords: List[String]): T = keywords.zipWithIndex.map { case (keyword, i) => isabelle.JSON.Object("id" -> i, "keyword" -> keyword) } } /* keyword extraction */ private val replacements = List( "<[^>]*>".r -> "", "[^\\w\\s()'.,;:-]".r -> " ", "\\s+".r -> " ") def extract_keywords(text: String): List[String] = { val stripped_text = replacements.foldLeft(text) { case (res, (regex, replacement)) => regex.replaceAllIn(res, replacement) } val arg = quote(stripped_text.replaceAll("\"", "\\\"")) val keyword_cmd = "from keywords import *; print_keywords(" + arg + ")" Python.run(keyword_cmd).check.out_lines } /* site generation */ def afp_site_gen( out_dir: Option[Path], layout: Hugo.Layout, afp_structure: AFP_Structure, progress: Progress = new Progress()): Unit = { /* add authors */ progress.echo("Preparing authors...") val authors = afp_structure.load_authors val authors_by_id = Utils.grouped_sorted(authors, (a: Metadata.Author) => a.id) layout.write_data(Path.basic("authors.json"), JSON.from_authors(authors)) /* add topics */ progress.echo("Preparing topics...") val topics = afp_structure.load_topics def sub_topics(topic: Metadata.Topic): List[Metadata.Topic] = topic :: topic.sub_topics.flatMap(sub_topics) val topics_by_id = Utils.grouped_sorted(topics.flatMap(sub_topics), (t: Metadata.Topic) => t.id) layout.write_data(Path.basic("topics.json"), JSON.from_topics(topics)) /* add releases */ progress.echo("Preparing releases...") val releases_by_entry = afp_structure.load_releases.groupBy(_.entry) /* extract keywords */ progress.echo("Extracting keywords...") var seen_keywords = Set.empty[String] val entry_keywords = afp_structure.entries.map(name => { val entry = afp_structure.load_entry(name, authors_by_id, topics_by_id, releases_by_entry) val Keyword = """\('([^']*)', ([^)]*)\)""".r val scored_keywords = extract_keywords(entry.`abstract`).map { case Keyword(keyword, score) => keyword -> score.toDouble case s => error("Could not parse: " + s) } seen_keywords ++= scored_keywords.map(_._1) name -> scored_keywords.filter(_._2 > 1.0).map(_._1) }).toMap seen_keywords = seen_keywords.filter(k => !k.endsWith("s") || !seen_keywords.contains(k.stripSuffix("s"))) layout.write_static(Path.make(List("data", "keywords.json")), JSON.from_keywords(seen_keywords.toList)) def get_keywords(name: Metadata.Entry.Name): List[String] = entry_keywords(name).filter(seen_keywords.contains).take(8) /* add entries and theory listings */ progress.echo("Preparing entries...") val sessions_structure = afp_structure.sessions_structure val sessions_deps = Sessions.deps(sessions_structure) for (name <- afp_structure.entries) { val entry = afp_structure.load_entry(name, authors_by_id, topics_by_id, releases_by_entry) val deps = for { session <- afp_structure.entry_sessions(name) dep <- sessions_structure.imports_graph.imm_preds(session.name) if session.name != dep && sessions_structure(dep).groups.contains("AFP") } yield dep val topo_theories = for { session <- afp_structure.entry_sessions(name) base = sessions_deps(session.name) node <- base.session_theories } yield node.theory_base_name val entry_json = JSON.from_entry(entry) ++ isabelle.JSON.Object( "dependencies" -> deps.distinct, "theories" -> topo_theories, - "aliases" -> List("/entries/" + name + ".html"), + "url" -> ("/entries/" + name + ".html"), "keywords" -> get_keywords(name)) val theories_json = isabelle.JSON.Object( "title" -> entry.title, "url" -> ("/entries/" + name.toLowerCase + "/theories"), "theories" -> topo_theories) layout.write_content(Path.make(List("entries", name + ".md")), entry_json) layout.write_content(Path.make(List("theories", name + ".md")), theories_json) } /* add statistics */ progress.echo("Preparing statistics...") val statistics_cmd = "from statistics import *; add_statistics(" + commas_quote( List( Path.explode("$AFP_BASE").absolute.implode, Path.explode("$AFP").absolute.implode, layout.data_dir.implode)) + ")" Python.run(statistics_cmd).check (layout.data_dir + Path.basic("statistics.html")).file.delete() /* project */ progress.echo("Preparing project files") layout.copy_project() /* hugo */ out_dir match { case Some(out_dir) => progress.echo("Building site...") Hugo.build(layout, out_dir).check progress.echo("Finished building site") case None => progress.echo("Finished sitegen preparation.") } } val isabelle_tool = Isabelle_Tool("afp_site_gen", "generates afp website source", Scala_Project.here, args => { var base_dir = Path.explode("$AFP_BASE") var hugo_dir = base_dir + Path.make(List("web", "hugo")) var out_dir: Option[Path] = None val getopts = Getopts(""" Usage: isabelle afp_site_gen [OPTIONS] Options are: -B DIR afp base dir (default """" + base_dir.implode + """") -H DIR generated hugo project dir (default """" + hugo_dir.implode + """") -O DIR output dir (default none) Generates the AFP website source. HTML files of entries are dynamically loaded. Site will be built from generated source if output dir is specified. """, "B:" -> (arg => base_dir = Path.explode(arg)), "H:" -> (arg => hugo_dir = Path.explode(arg)), "O:" -> (arg => out_dir = Some(Path.explode(arg)))) getopts(args) val afp_structure = AFP_Structure(base_dir) val layout = Hugo.Layout(hugo_dir) val progress = new Console_Progress() progress.echo("Preparing site generation in " + hugo_dir.implode) afp_site_gen(out_dir = out_dir, layout = layout, afp_structure = afp_structure, progress = progress) }) } \ No newline at end of file