diff --git a/web/js/theory.js b/web/js/theory.js --- a/web/js/theory.js +++ b/web/js/theory.js @@ -1,279 +1,283 @@ /* 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 `../${href_parts[1].toLowerCase()}/#${href_parts[2]}` + if (href_parts.length === 1) { + const ref_parts = href_parts[0].split('.html') + const file_parts = ref_parts[0].split('.') + if (file_parts.length == 1) return `#${href_parts[0]}` + else { + return `../${file_parts[0].toLowerCase()}/#${file_parts.slice(1).join('.')}.html${ref_parts[1]}` + } } 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_fresh_id = (id) => `${id}#` const to_svg_id = (id) => `${id}#svg` const to_container_id = (id) => `${id}#container` const to_collapsible_id = (id) => `${id}#collapsible` const to_spinner_id = (id) => `${id}#spinner` const to_nav_id = (id) => `${id}#nav` const to_ul_id = (id) => `${id}#ul` const of_ul_id = (id) => id.split('#').slice(0, -1).join('#') const to_a_id = (id) => `${id}#a` /* 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_fresh_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 ref = `${path.join('.')}.${key}|${type}` const id = to_id(thy_name, ref) 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} ` } 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(` `) } 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) ScrollSpy.instance.scroll_to(id) } } 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}
    • `))) navbar.insertAdjacentElement('afterend', document.createElement('hr')); 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/web/submission/index.html b/web/submission/index.html --- a/web/submission/index.html +++ b/web/submission/index.html @@ -1,126 +1,127 @@ Entry Submission - Archive of Formal Proofs

    Entry Submission

    Submission Guidelines

    The submission must follow the following Isabelle style rules. For additional guidelines on Isabelle proofs, also see the this guide (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 chapter AFP, and all theory files of the submission must be contained in at least one session. See also the example ROOT file in the Example submission.
    • The entry should cite all sources that the theories are based on, for example textbooks or research articles containing informal versions of the proofs.
      • +
    • All sessions must have a timeout after which they are assumed to be in a non-terminating state. Timeouts may be no finer than five-minute increments, i.e. must be divisible by 300.

    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.

    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 in your theories.

    Submission Form

    Submission form

    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. If you need help with Isabelle, please use the isabelle-users@cl.cam.ac.uk mailing list. It is always a good idea to subscribe.

    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 or as tar.gz package on the download page.
    • 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.

    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 of your AFP entry and test it against the current Isabelle development version.

    If you would like to get write access to your entry in the mercurial repository or if you need assistance, please contact the editors.

    \ No newline at end of file