From 6dbc6f0c0fe760b07d1dd691f8ed34c76f878835 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Tue, 10 Nov 2020 09:41:21 +0200 Subject: [PATCH 01/25] setup branch --- nav.js | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/nav.js b/nav.js index def1be7..89ab599 100644 --- a/nav.js +++ b/nav.js @@ -116,23 +116,22 @@ const declSearch = (q) => new Promise((resolve, reject) => { const srId = 'search_results'; document.getElementById('search_form') .appendChild(document.createElement('div')) - .id = srId; + .id = srId; // todo add on creation of page, not here -function goToDecl(d) { window.location.href = `${siteRoot}find/${d}`; } +function goToDecl(d) { + window.location.href = `${siteRoot}find/${d}`; +} function handleSearchCursorUpDown(down) { const sel = document.querySelector(`#${srId} .selected`); const sr = document.getElementById(srId); + + let toSelect = down ? sr.firstChild : sr.lastChild; if (sel) { sel.classList.remove('selected'); - const toSelect = down ? - sel.nextSibling || sr.firstChild: - sel.previousSibling || sr.lastChild; - toSelect && toSelect.classList.add('selected'); - } else { - const toSelect = down ? sr.firstChild : sr.lastChild; - toSelect && toSelect.classList.add('selected'); + toSelect = down ? sel.nextSibling : sel.previousSibling; } + toSelect && toSelect.classList.add('selected'); } function handleSearchEnter() { @@ -175,7 +174,7 @@ searchInput.addEventListener('input', async (ev) => { document.getElementById(srId).setAttribute('state', 'loading'); const result = await declSearch(text); - if (ev.target.value != text) return; + if (ev.target.value != text) return; // todo why? const oldSR = document.getElementById('search_results'); const sr = oldSR.cloneNode(false); From c6711a75decdb14bb1b465443568106160544c24 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Fri, 11 Dec 2020 21:21:41 +0200 Subject: [PATCH 02/25] improve code readability --- nav.js | 171 +++++++++++++++++++++++++----------------------------- style.css | 2 +- 2 files changed, 79 insertions(+), 94 deletions(-) diff --git a/nav.js b/nav.js index ec886da..6d39d94 100644 --- a/nav.js +++ b/nav.js @@ -26,119 +26,109 @@ for (const elem of document.getElementsByClassName('nav_sect')) { } for (const currentFileLink of document.getElementsByClassName('visible')) { - currentFileLink.scrollIntoView({block: 'center'}); + currentFileLink.scrollIntoView({ block: 'center' }); } - - - - - // Tactic list tag filter -// ---------------------- +// ---------------------- -function filterSelectionClass(tagNames, classname) { - if (tagNames.length == 0) { - for (const elem of document.getElementsByClassName(classname)) { - elem.classList.remove("hide"); - } - } else { - // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected - for (const elem of document.getElementsByClassName(classname)) { - elem.classList.add("hide"); - for (const tagName of tagNames) { - if (elem.classList.contains(tagName)) { - elem.classList.remove("hide"); - } +function filterSelectionClass(tagNames, className) { + if (tagNames.length === 0) { + for (const elem of document.getElementsByClassName(className)) { + elem.classList.remove("hide"); + } + } else { + // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected + for (const elem of document.getElementsByClassName(className)) { + elem.classList.add("hide"); + for (const tagName of tagNames) { + if (elem.classList.contains(tagName)) { + elem.classList.remove("hide"); } } } } +} - function filterSelection(c) { - filterSelectionClass(c, "tactic"); - filterSelectionClass(c, "taclink"); - } +function filterSelection(c) { + filterSelectionClass(c, "tactic"); + filterSelectionClass(c, "taclink"); +} -var filterBoxes = document.getElementsByClassName("tagfilter"); +var filterBoxesElmnts = document.getElementsByClassName("tagfilter"); function updateDisplay() { - filterSelection(getSelectValues()); + filterSelection(getSelectValues()); } function getSelectValues() { - var result = []; - - for (const opt of filterBoxes) { - - if (opt.checked) { - result.push(opt.value); - } + var result = []; + for (const opt of filterBoxesElmnts) { + if (opt.checked) { + result.push(opt.value); } - return result; } + return result; +} function setSelectVal(val) { - for (const opt of filterBoxes) { + for (const opt of filterBoxesElmnts) { opt.checked = val; } } updateDisplay(); -for (const opt of filterBoxes) { +for (const opt of filterBoxesElmnts) { opt.addEventListener('change', updateDisplay); } -const tse = document.getElementById("tagfilter-selectall") -if (tse != null) { - tse.addEventListener('change', function() { +const tse = document.getElementById("tagfilter-selectall"); +if (tse !== null) { + tse.addEventListener('change', function () { setSelectVal(this.checked); updateDisplay(); }); } - - - -// Simple declaration search +// Simple search through declarations by name // ------------------------- const searchWorkerURL = new URL(`${siteRoot}searchWorker.js`, window.location); -const declSearch = (q) => new Promise((resolve, reject) => { +const declSearch = (query) => new Promise((resolve, reject) => { const worker = new SharedWorker(searchWorkerURL); worker.port.start(); - worker.port.onmessage = ({data}) => resolve(data); + worker.port.onmessage = ({ data }) => resolve(data); worker.port.onmessageerror = (e) => reject(e); - worker.port.postMessage({q}); + worker.port.postMessage({ query }); }); -const srId = 'search_results'; +const resultsElmntId = 'search_results'; document.getElementById('search_form') .appendChild(document.createElement('div')) - .id = srId; // todo add on creation of page, not here + .id = resultsElmntId; // todo add on creation of page, not here function handleSearchCursorUpDown(down) { - const sel = document.querySelector(`#${srId} .selected`); - const sr = document.getElementById(srId); + const selectedResult = document.querySelector(`#${resultsElmntId} .selected`); + const resultsElmnt = document.getElementById(resultsElmntId); - let toSelect = down ? sr.firstChild : sr.lastChild; - if (sel) { - sel.classList.remove('selected'); - toSelect = down ? sel.nextSibling : sel.previousSibling; + let toSelect = down ? resultsElmnt.firstChild : resultsElmnt.lastChild; + if (selectedResult) { + selectedResult.classList.remove('selected'); + toSelect = down ? selectedResult.nextSibling : selectedResult.previousSibling; } toSelect && toSelect.classList.add('selected'); } -function handleSearchEnter() { - const sel = document.querySelector(`#${srId} .selected`) - || document.getElementById(srId).firstChild; - sel.click(); +function handleSearchItemSelected() { + const selectedResult = document.querySelector(`#${resultsElmntId} .selected`) + selectedResult.click(); } -const searchInput = document.querySelector('#search_form input[name=q]'); +const searchInputElmnt = document.querySelector('#search_form input[name=q]'); -searchInput.addEventListener('keydown', (ev) => { +// todo use Enter to start searching if we still in and not
+searchInputElmnt.addEventListener('keydown', (ev) => { switch (ev.key) { case 'Down': case 'ArrowDown': @@ -152,64 +142,59 @@ searchInput.addEventListener('keydown', (ev) => { break; case 'Enter': ev.preventDefault(); - handleSearchEnter(); + handleSearchItemSelected(); break; } }); -searchInput.addEventListener('input', async (ev) => { +searchInputElmnt.addEventListener('input', async (ev) => { const text = ev.target.value; if (!text) { - const sr = document.getElementById(srId); - sr.removeAttribute('state'); - sr.replaceWith(sr.cloneNode(false)); + const resultsElmnt = document.getElementById(resultsElmntId); + resultsElmnt.removeAttribute('state'); + resultsElmnt.replaceWith(resultsElmnt.cloneNode(false)); return; } - document.getElementById(srId).setAttribute('state', 'loading'); + document.getElementById(resultsElmntId).setAttribute('state', 'loading'); const result = await declSearch(text); if (ev.target.value != text) return; // todo why? - const oldSR = document.getElementById('search_results'); - const sr = oldSR.cloneNode(false); - for (const {decl} of result) { - const d = sr.appendChild(document.createElement('a')); + const currentResultsElmnt = document.getElementById('search_results'); + const resultsElmntCopy = currentResultsElmnt.cloneNode(false); + for (const { decl } of result) { + const d = resultsElmntCopy.appendChild(document.createElement('a')); d.innerText = decl; d.title = decl; - d.href = `${siteRoot}find/${decl}`; + d.href = `${siteRoot}find/${decl}`; // todo why not a link directly to the declaration in docs? } - sr.setAttribute('state', 'done'); - oldSR.replaceWith(sr); + resultsElmntCopy.setAttribute('state', 'done'); + currentResultsElmnt.replaceWith(resultsElmntCopy); }); - - - - - // 404 page goodies // ---------------- -const howabout = document.getElementById('howabout'); -if (howabout) { - howabout.innerText = "Please wait a second. I'll try to help you."; +const suggestionsElmnt = document.getElementById('howabout'); +if (suggestionsElmnt) { + suggestionsElmnt.innerText = "Please wait a second. I'll try to help you."; - howabout.parentNode - .insertBefore(document.createElement('pre'), howabout) - .appendChild(document.createElement('code')) - .innerText = window.location.href.replace(/[/]/g, '/\u200b'); + suggestionsElmnt.parentNode + .insertBefore(document.createElement('pre'), suggestionsElmnt) + .appendChild(document.createElement('code')) + .innerText = window.location.href.replace(/[/]/g, '/\u200b'); const query = window.location.href.match(/[/]([^/]+)(?:\.html|[/])?$/)[1]; declSearch(query).then((results) => { - howabout.innerText = 'How about one of these instead:'; - const ul = howabout.appendChild(document.createElement('ul')); - for (const {decl} of results) { - const li = ul.appendChild(document.createElement('li')); - const a = li.appendChild(document.createElement('a')); - a.href = `${siteRoot}find/${decl}`; - a.appendChild(document.createElement('code')).innerText = decl; - } + suggestionsElmnt.innerText = 'How about one of these instead:'; + const ul = suggestionsElmnt.appendChild(document.createElement('ul')); + for (const { decl } of results) { + const li = ul.appendChild(document.createElement('li')); + const a = li.appendChild(document.createElement('a')); + a.href = `${siteRoot}find/${decl}`; // todo why not a link directly? + a.appendChild(document.createElement('code')).innerText = decl; + } }); } diff --git a/style.css b/style.css index ee5c8c4..e4ce67b 100644 --- a/style.css +++ b/style.css @@ -170,7 +170,7 @@ header header_filename { } #search_results[state="loading"]:empty::before { display: block; - content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; + content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; padding: 1ex; animation: marquee 10s linear infinite; } From e23988f321fad47c6ac28925f66744a93749f992 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Sat, 19 Dec 2020 13:53:58 +0200 Subject: [PATCH 03/25] minor fixes --- print_docs.py | 11 ++++++----- searchWorker.js | 1 + 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/print_docs.py b/print_docs.py index 565c739..7f3f832 100644 --- a/print_docs.py +++ b/print_docs.py @@ -31,8 +31,8 @@ from jinja2 import Environment, FileSystemLoader, select_autoescape env = Environment( - loader=FileSystemLoader('templates', 'utf-8'), - autoescape=select_autoescape(['html', 'xml']) + loader=FileSystemLoader('templates', 'utf-8'), + autoescape=select_autoescape(['html', 'xml']) ) env.globals['sorted'] = sorted @@ -209,11 +209,12 @@ def separate_results(objs): i_name = obj['filename'] = ImportName.of(obj['filename']) if i_name.project == '.': continue # this is doc-gen itself + file_map[i_name].append(obj) loc_map[obj['name']] = i_name - for (cstr_name, tp) in obj['constructors']: + for (cstr_name, _) in obj['constructors']: loc_map[cstr_name] = i_name - for (sf_name, tp) in obj['structure_fields']: + for (sf_name, _) in obj['structure_fields']: loc_map[sf_name] = i_name if len(obj['structure_fields']) > 0: loc_map[obj['name'] + '.mk'] = i_name @@ -523,7 +524,7 @@ def mk_export_map_entry(decl_name, filename, kind, is_meta, line, args, tp): def mk_export_db(loc_map, file_map): export_db = {} - for fn, decls in file_map.items(): + for _, decls in file_map.items(): for obj in decls: export_db[obj['name']] = mk_export_map_entry(obj['name'], obj['filename'], obj['kind'], obj['is_meta'], obj['line'], obj['args'], obj['type']) export_db[obj['name']]['decl_header_html'] = env.get_template('decl_header.j2').render(decl=obj) diff --git a/searchWorker.js b/searchWorker.js index f1efa5f..6b65a26 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -1,3 +1,4 @@ +// todo why such a fetch since file is already present here? const req = new XMLHttpRequest(); req.open('GET', 'decl.txt', false /* blocking */); req.responseType = 'text'; From c48b29353bbf8ac290c3b5ede6d4fd60b38f6cb1 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Sat, 16 Jan 2021 18:04:44 +0200 Subject: [PATCH 04/25] python script readability improvements --- import_name.py | 60 ++++++ leanpkg.toml | 2 +- print_docs.py | 574 +++++++++++++++++++++++-------------------------- 3 files changed, 329 insertions(+), 307 deletions(-) create mode 100644 import_name.py diff --git a/import_name.py b/import_name.py new file mode 100644 index 0000000..26f9e1c --- /dev/null +++ b/import_name.py @@ -0,0 +1,60 @@ +import subprocess +from typing import NamedTuple, List +from pathlib import Path +import json +import toml + +class ImportName(NamedTuple): + project: str + parts: List[str] + raw_path: Path + + @classmethod + def of(cls, fname: str): + fname = Path(fname) + path_info = [(p.resolve(), get_name_from_leanpkg_path(p)) for p in lean_paths] + path_details = "".join(f" - {p}\n" for p, _ in path_info) + + for p, name in path_info: + try: + rel_path = fname.relative_to(p) + except ValueError: + pass + else: + return cls(name, rel_path.with_suffix('').parts, fname) + + raise RuntimeError( + f"Cannot determine import name for {fname}; it is not within any of the directories returned by `lean --path`:\n" + f"{path_details}" + f"Did you generate `export.json` using a different Lean installation to the one this script is running with?") + + @property + def name(self): + return '.'.join(self.parts) + + @property + def url(self): + return '/'.join(self.parts) + '.html' + +def get_name_from_leanpkg_path(p: Path) -> str: + """ get the package name corresponding to a source path """ + if p.parts[-5:] == Path('bin/../lib/lean/library').parts or p.parts[-3:] == Path('bin/../library').parts: + return "core" + + # try the toml + p_leanpkg = p / '..' / 'leanpkg.toml' + try: + f = p_leanpkg.open() + except FileNotFoundError: + pass + else: + with f: + parsed_toml = toml.loads(f.read()) + return parsed_toml['package']['name'] + + return '' + +lean_paths = [ + Path(p) + for p in json.loads(subprocess.check_output(['lean', '--path']).decode())['path'] +] diff --git a/leanpkg.toml b/leanpkg.toml index 9fd0b8a..c29fc17 100644 --- a/leanpkg.toml +++ b/leanpkg.toml @@ -5,4 +5,4 @@ lean_version = "leanprover-community/lean:3.23.0" path = "src" [dependencies] -mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "5a61ef1981738b829ff712cab18e63a675108c40"} +mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "5a61ef1981738b829ff712cab18e63a675108c40"} \ No newline at end of file diff --git a/print_docs.py b/print_docs.py index 7f3f832..35d62cc 100644 --- a/print_docs.py +++ b/print_docs.py @@ -4,202 +4,82 @@ # `pip install markdown2 toml` # -import json +# interpreter and general external access +import sys import os import os.path +import argparse +import subprocess +from jinja2 import Environment, FileSystemLoader, select_autoescape + +# directories manipulation +import shutil +import gzip + +# data structures +from pathlib import Path +from typing import List +from collections import defaultdict +from import_name import ImportName + +# data structures manipulation +import json +import toml import glob +import re import textwrap import markdown2 -import re -import subprocess -import toml -import shutil -import argparse import html -import gzip from urllib.parse import quote from functools import reduce -import textwrap -from collections import defaultdict -from pathlib import Path -from typing import NamedTuple, List -import sys - import networkx as nx -root = os.getcwd() - -from jinja2 import Environment, FileSystemLoader, select_autoescape -env = Environment( - loader=FileSystemLoader('templates', 'utf-8'), - autoescape=select_autoescape(['html', 'xml']) -) -env.globals['sorted'] = sorted - +# get arguments from script inititation parser = argparse.ArgumentParser('Options to print_docs.py') parser.add_argument('-w', help = 'Specify site root URL') parser.add_argument('-l', help = 'Symlink CSS and JS instead of copying', action = "store_true") parser.add_argument('-r', help = 'relative path to mathlib root directory') parser.add_argument('-t', help = 'relative path to html output directory') -cl_args = parser.parse_args() +CLI_ARGS = parser.parse_args() + +# setup templates environment +env = Environment( + loader=FileSystemLoader('templates', 'utf-8'), + autoescape=select_autoescape(['html', 'xml']) +) # extra doc files to include in generation # the content has moved to the community website, # but we still build them to avoid broken links # format: (filename_root, display_name, source, community_site_url) -extra_doc_files = [('overview', 'mathlib overview', 'docs/mathlib-overview.md', 'mathlib-overview'), - ('tactic_writing', 'tactic writing', 'docs/extras/tactic_writing.md', 'extras/tactic_writing'), - ('calc', 'calc mode', 'docs/extras/calc.md', 'extras/calc'), - ('conv', 'conv mode', 'docs/extras/conv.md', 'extras/conv'), - ('simp', 'simplification', 'docs/extras/simp.md', 'extras/simp'), - ('well_founded_recursion', 'well founded recursion', 'docs/extras/well_founded_recursion.md','extras/well_founded_recursion'), - ('style', 'style guide', 'docs/contribute/style.md','contribute/style'), - ('doc_style', 'documentation style guide', 'docs/contribute/doc.md','contribute/doc'), - ('naming', 'naming conventions', 'docs/contribute/naming.md','contribute/naming')] -env.globals['extra_doc_files'] = extra_doc_files - -# path to put generated html -html_root = os.path.join(root, cl_args.t if cl_args.t else 'html') + '/' - -# TODO: make sure nothing is left in html_root - -# root of the site, for display purposes. -# override this setting with the `-w` flag. -site_root = "/" - -# root directory of mathlib. -local_lean_root = os.path.join(root, cl_args.r if cl_args.r else '_target/deps/mathlib') + '/' +# TODO: avoid broken links and remove unnecessary structures and action +EXTRA_DOC_FILES = [ + ('overview', 'mathlib overview', 'docs/mathlib-overview.md', 'mathlib-overview'), + ('tactic_writing', 'tactic writing', 'docs/extras/tactic_writing.md', 'extras/tactic_writing'), + ('calc', 'calc mode', 'docs/extras/calc.md', 'extras/calc'), + ('conv', 'conv mode', 'docs/extras/conv.md', 'extras/conv'), + ('simp', 'simplification', 'docs/extras/simp.md', 'extras/simp'), + ('well_founded_recursion', 'well founded recursion', 'docs/extras/well_founded_recursion.md','extras/well_founded_recursion'), + ('style', 'style guide', 'docs/contribute/style.md','contribute/style'), + ('doc_style', 'documentation style guide', 'docs/contribute/doc.md','contribute/doc'), + ('naming', 'naming conventions', 'docs/contribute/naming.md','contribute/naming') +] +# setup global variables +ROOT = os.getcwd() +SITE_ROOT = CLI_ARGS.w if CLI_ARGS.w else "/" +MATHLIB_SRC_ROOT = os.path.join(ROOT, CLI_ARGS.r if CLI_ARGS.r else '_target/deps/mathlib') + '/' +MATHLIB_DEST_ROOT = os.path.join(ROOT, CLI_ARGS.t if CLI_ARGS.t else 'html', '') # TODO: make sure nothing is left in docs_destination_root +LINK_PATTERNS = [(re.compile(r'Note \[(.*)\]', re.I), SITE_ROOT + r'notes.html#\1')] +LEAN_COMMIT = subprocess.check_output(['lean', '--run', 'src/lean_commit.lean']).decode() with open('leanpkg.toml') as f: parsed_toml = toml.loads(f.read()) ml_data = parsed_toml['dependencies']['mathlib'] -mathlib_commit = ml_data['rev'] -mathlib_github_root = ml_data['git'].strip('/') - -if cl_args.w: - site_root = cl_args.w - -mathlib_github_src_root = "{0}/blob/{1}/src/".format(mathlib_github_root, mathlib_commit) - -lean_commit = subprocess.check_output(['lean', '--run', 'src/lean_commit.lean']).decode() -lean_root = 'https://github.com/leanprover-community/lean/blob/{}/library/'.format(lean_commit) - -def get_name_from_leanpkg_path(p: Path) -> str: - """ get the package name corresponding to a source path """ - # lean core? - if p.parts[-5:] == Path('bin/../lib/lean/library').parts: - return "core" - if p.parts[-3:] == Path('bin/../library').parts: - return "core" - - # try the toml - p_leanpkg = p / '..' / 'leanpkg.toml' - try: - f = p_leanpkg.open() - except FileNotFoundError: - pass - else: - with f: - parsed_toml = toml.loads(f.read()) - return parsed_toml['package']['name'] - - return '' - -lean_paths = [ - Path(p) - for p in json.loads(subprocess.check_output(['lean', '--path']).decode())['path'] -] -path_info = [(p.resolve(), get_name_from_leanpkg_path(p)) for p in lean_paths] - -class ImportName(NamedTuple): - project: str - parts: List[str] - raw_path: Path - - @classmethod - def of(cls, fname: str): - fname = Path(fname) - for p, name in path_info: - try: - rel_path = fname.relative_to(p) - except ValueError: - pass - else: - return cls(name, rel_path.with_suffix('').parts, fname) - path_details = "".join(f" - {p}\n" for p, _ in path_info) - raise RuntimeError( - f"Cannot determine import name for {fname}; it is not within any of the directories returned by `lean --path`:\n" - f"{path_details}" - f"Did you generate `export.json` using a different Lean installation to the one this script is running with?") - - @property - def name(self): - return '.'.join(self.parts) - - @property - def url(self): - return '/'.join(self.parts) + '.html' - -env.globals['mathlib_github_root'] = mathlib_github_root -env.globals['mathlib_commit'] = mathlib_commit -env.globals['lean_commit'] = lean_commit -env.globals['site_root'] = site_root - -note_regex = re.compile(r'Note \[(.*)\]', re.I) -target_url_regex = site_root + r'notes.html#\1' -link_patterns = [(note_regex, target_url_regex)] +MATHLIB_COMMIT = ml_data['rev'] +MATHLIB_GITHUB_ROOT = ml_data['git'].strip('/') -def convert_markdown(ds, toc=False): - extras = ['code-friendly', 'cuddled-lists', 'fenced-code-blocks', 'link-patterns', 'tables'] - if toc: - extras.append('toc') - return markdown2.markdown(ds, extras=extras, link_patterns = link_patterns) - -# TODO: allow extending this for third-party projects -library_link_roots = { - 'core': lean_root, - 'mathlib': mathlib_github_src_root, -} - -def library_link(filename: ImportName, line=None): - try: - root = library_link_roots[filename.project] - except KeyError: - return "" # empty string is handled as a self-link - - root += '/'.join(filename.parts) + '.lean' - if line is not None: - root += f'#L{line}' - return root - -env.globals['library_link'] = library_link -env.filters['library_link'] = library_link - -def name_in_decl(decl_name, dmap): - if dmap['name'] == decl_name: - return True - if decl_name in [sf[0] for sf in dmap['structure_fields']]: - return True - if decl_name in [sf[0] for sf in dmap['constructors']]: - return True - return False - -def library_link_from_decl_name(decl_name, decl_loc, file_map): - try: - e = next(d for d in file_map[decl_loc] if name_in_decl(decl_name, d)) - except StopIteration as e: - if decl_name[-3:] == '.mk': - return library_link_from_decl_name(decl_name[:-3], decl_loc, file_map) - print(f'{decl_name} appears in {decl_loc}, but we do not have data for that declaration. file_map:') - print(file_map[decl_loc]) - raise e - return library_link(decl_loc, e['line']) - -def open_outfile(filename, mode = 'w'): - filename = os.path.join(html_root, filename) - os.makedirs(os.path.dirname(filename), exist_ok=True) - return open(filename, mode, encoding='utf-8') +# ------------------------------------------------ START utils reading ------------------------------------------------- def separate_results(objs): file_map = defaultdict(list) @@ -220,6 +100,46 @@ def separate_results(objs): loc_map[obj['name'] + '.mk'] = i_name return file_map, loc_map +# ------------------------------------------------ END utils reading --------------------------------------------------- + + +# ------------------------------------------------ START read source files ------------------------------------------------- + +def read_src_data(): + with open('export.json', 'r', encoding='utf-8') as f: + decls = json.load(f, strict=False) + file_map, loc_map = separate_results(decls['decls']) + for entry in decls['tactic_docs']: + if len(entry['tags']) == 0: + entry['tags'] = ['untagged'] + + mod_docs = {ImportName.of(f): docs for f, docs in decls['mod_docs'].items()} + # ensure the key is present for `default.lean` modules with no declarations + for i_name in mod_docs: + if i_name.project == '.': + continue # this is doc-gen itself + file_map[i_name] + + return file_map, loc_map, decls['notes'], mod_docs, decls['instances'], decls['tactic_docs'] + +# ------------------------------------------------ END read source files ----------------------------------------------------- + +# ------------------------------------------------ START common utils -------------------------------------------------------- + +def convert_markdown(ds, toc=False): + extras = ['code-friendly', 'cuddled-lists', 'fenced-code-blocks', 'link-patterns', 'tables'] + if toc: + extras.append('toc') + return markdown2.markdown(ds, extras=extras, link_patterns = LINK_PATTERNS) + +# returns (pagetitle, intro_block), [(tactic_name, tactic_block)] +def split_tactic_list(markdown): + entries = re.findall(r'(?<=# )(.*)([\s\S]*?)(?=(##|\Z))', markdown) + return entries[0], entries[1:] + +# ------------------------------------------------ END common utils ---------------------------------------------------------- + +# ------------------------------------------------ START templates setup ---------------------------------------------------- def trace_deps(file_map): graph = nx.DiGraph() import_name_by_path = {k.raw_path: k for k in file_map} @@ -240,43 +160,73 @@ def trace_deps(file_map): print(f"trace_deps: Processed {n_ok} / {n} dependency links") return graph -def load_json(): - with open('export.json', 'r', encoding='utf-8') as f: - decls = json.load(f, strict=False) - file_map, loc_map = separate_results(decls['decls']) - for entry in decls['tactic_docs']: - if len(entry['tags']) == 0: - entry['tags'] = ['untagged'] +def mk_site_tree(partition: List[ImportName]): + filenames = [ [filename.project] + list(filename.parts) for filename in partition ] + return mk_site_tree_core(filenames) - mod_docs = {ImportName.of(f): docs for f, docs in decls['mod_docs'].items()} - # ensure the key is present for `default.lean` modules with no declarations - for i_name in mod_docs: - if i_name.project == '.': - continue # this is doc-gen itself - file_map[i_name] +def mk_site_tree_core(filenames, path=[]): + entries = [] - return file_map, loc_map, decls['notes'], mod_docs, decls['instances'], decls['tactic_docs'] + for dirname in sorted(set(dirname for dirname, *rest in filenames if rest != [])): + new_path = path + [dirname] + entries.append({ + "kind": "project" if not path else "dir", + "name": dirname, + "path": '/'.join(new_path[1:]), + "children": mk_site_tree_core([rest for dn, *rest in filenames if rest != [] and dn == dirname], new_path) + }) + + for filename in sorted(filename for filename, *rest in filenames if rest == []): + new_path = path + [filename] + entries.append({ + "kind": "file", + "name": filename, + "path": '/'.join(new_path[1:]) + '.html', + }) + + return entries + +def import_options(loc_map, decl_name, import_string): + direct_import_paths = [] + if decl_name in loc_map: + direct_import_paths.append(loc_map[decl_name].name) + if import_string != '' and import_string not in direct_import_paths: + direct_import_paths.append(import_string) + if any(i.startswith('init.') for i in direct_import_paths): + return '
Import using
    {}
'.format('
  • imported by default
  • ') + elif len(direct_import_paths) > 0: + return '
    Import using
      {}
    '.format( + '\n'.join(['
  • import {}
  • '.format(d) for d in direct_import_paths])) + else: + return '' + +def kind_of_decl(decl): + kind = 'structure' if len(decl['structure_fields']) > 0 else 'inductive' if len(decl['constructors']) > 0 else decl['kind'] + if kind == 'thm': kind = 'theorem' + elif kind == 'cnst': kind = 'constant' + elif kind == 'ax': kind = 'axiom' + return kind + +def tag_id_of_name(tag): + return tag.strip().replace(' ', '-') def linkify_core(decl_name, text, loc_map): if decl_name in loc_map: tooltip = ' title="{}"'.format(decl_name) if text != decl_name else '' return '{2}'.format( - site_root + loc_map[decl_name].url, decl_name, text, tooltip) + SITE_ROOT + loc_map[decl_name].url, decl_name, text, tooltip) elif text != decl_name: return '{1}'.format(decl_name, text) else: return text -def linkify(string, loc_map): - return linkify_core(string, string, loc_map) - -def linkify_linked(string, loc_map): - return ''.join( - match[4] if match[0] == '' else - match[1] + linkify_core(match[0], match[2], loc_map) + match[3] - for match in re.findall(r'\ue000(.+?)\ue001(\s*)(.*?)(\s*)\ue002|([^\ue000]+)', string)) - def linkify_efmt(f, loc_map): + def linkify_linked(string, loc_map): + return ''.join( + match[4] if match[0] == '' else + match[1] + linkify_core(match[0], match[2], loc_map) + match[3] + for match in re.findall(r'\ue000(.+?)\ue001(\s*)(.*?)(\s*)\ue002|([^\ue000]+)', string)) + def go(f): if isinstance(f, str): f = f.replace('\n', ' ') @@ -294,7 +244,7 @@ def go(f): def linkify_markdown(string, loc_map): def linkify_type(string): splitstr = re.split(r'([\s\[\]\(\)\{\}])', string) - tks = map(lambda s: linkify(s, loc_map), splitstr) + tks = map(lambda s: linkify_core(s, s, loc_map), splitstr) return "".join(tks) string = re.sub(r'([^<]+)', @@ -303,6 +253,9 @@ def linkify_type(string): lambda p: '{}'.format(linkify_type(p.group(1))), string) return string +def link_to_decl(decl_name, loc_map): + return f'{SITE_ROOT}{loc_map[decl_name].url}#{decl_name}' + def plaintext_summary(markdown, max_chars = 200): # collapse lines text = re.compile(r'([a-zA-Z`(),;\$\-]) *\n *([a-zA-Z`()\$])').sub(r'\1 \2', markdown) @@ -320,7 +273,8 @@ def plaintext_summary(markdown, max_chars = 200): ] remove_patterns = [ r'^\s{0,3}>\s?', r'^={2,}', r'`{3}.*$', r'~~', r'^[=\-]{2,}\s*$', - r'^-{3,}\s*$', r'^\s*'] + r'^-{3,}\s*$', r'^\s*' + ] text = reduce(lambda text, p: re.compile(p, re.MULTILINE).sub(r'\1', text), remove_keep_contents_patterns, text) text = reduce(lambda text, p: re.compile(p, re.MULTILINE).sub('', text), remove_patterns, text) @@ -329,51 +283,67 @@ def plaintext_summary(markdown, max_chars = 200): text = re.compile(r'\s*\.?\n').sub('. ', text) return textwrap.shorten(text, width = max_chars, placeholder="…") + +def htmlify_name(n): + return '.'.join([f'{ html.escape(part) }' for part in n.split('.')]) -def link_to_decl(decl_name, loc_map): - return f'{site_root}{loc_map[decl_name].url}#{decl_name}' +def library_link(filename: ImportName, line=None): + mathlib_github_src_root = "{0}/blob/{1}/src/".format(MATHLIB_GITHUB_ROOT, MATHLIB_COMMIT) + lean_root = 'https://github.com/leanprover-community/lean/blob/{}/library/'.format(LEAN_COMMIT) -def kind_of_decl(decl): - kind = 'structure' if len(decl['structure_fields']) > 0 else 'inductive' if len(decl['constructors']) > 0 else decl['kind'] - if kind == 'thm': kind = 'theorem' - elif kind == 'cnst': kind = 'constant' - elif kind == 'ax': kind = 'axiom' - return kind -env.globals['kind_of_decl'] = kind_of_decl + # TODO: allow extending this for third-party projects + library_link_roots = { + 'core': lean_root, + 'mathlib': mathlib_github_src_root, + } -def htmlify_name(n): - return '.'.join([f'{ html.escape(part) }' for part in n.split('.')]) -env.filters['htmlify_name'] = htmlify_name + try: + root = library_link_roots[filename.project] + except KeyError: + return "" # empty string is handled as a self-link -# returns (pagetitle, intro_block), [(tactic_name, tactic_block)] -def split_tactic_list(markdown): - entries = re.findall(r'(?<=# )(.*)([\s\S]*?)(?=(##|\Z))', markdown) - return entries[0], entries[1:] + root += '/'.join(filename.parts) + '.lean' + if line is not None: + root += f'#L{line}' + return root -def import_options(loc_map, decl_name, import_string): - direct_import_paths = [] - if decl_name in loc_map: - direct_import_paths.append(loc_map[decl_name].name) - if import_string != '' and import_string not in direct_import_paths: - direct_import_paths.append(import_string) - if any(i.startswith('init.') for i in direct_import_paths): - return '
    Import using
      {}
    '.format('
  • imported by default
  • ') - elif len(direct_import_paths) > 0: - return '
    Import using
      {}
    '.format( - '\n'.join(['
  • import {}
  • '.format(d) for d in direct_import_paths])) - else: - return '' +def setup_jinja_env(file_map, loc_map, instances): + env.globals['import_graph'] = trace_deps(file_map) + env.globals['site_tree'] = mk_site_tree(file_map) + env.globals['instances'] = instances + env.globals['import_options'] = lambda d, i: import_options(loc_map, d, i) + env.globals['find_import_path'] = lambda d: find_import_path(loc_map, d) + env.globals['sorted'] = sorted + env.globals['extra_doc_files'] = EXTRA_DOC_FILES + env.globals['mathlib_github_root'] = MATHLIB_GITHUB_ROOT + env.globals['mathlib_commit'] = MATHLIB_COMMIT + env.globals['lean_commit'] = LEAN_COMMIT + env.globals['site_root'] = SITE_ROOT + env.globals['kind_of_decl'] = kind_of_decl + env.globals['tag_id_of_name'] = tag_id_of_name + env.globals['tag_ids_of_names'] = lambda names: ' '.join(tag_id_of_name(n) for n in names) + env.globals['library_link'] = library_link + + env.filters['linkify'] = lambda x: linkify_core(x, x, loc_map) + env.filters['linkify_efmt'] = lambda x: linkify_efmt(x, loc_map) + env.filters['convert_markdown'] = lambda x: linkify_markdown(convert_markdown(x), loc_map) # TODO: this is probably very broken + env.filters['link_to_decl'] = lambda x: link_to_decl(x, loc_map) + env.filters['plaintext_summary'] = plaintext_summary + env.filters['split_on_hr'] = lambda x: x.split('\n---\n', 1)[-1] + env.filters['htmlify_name'] = htmlify_name + env.filters['library_link'] = library_link -def split_on_hr(description): - return description.split('\n---\n', 1)[-1] -env.filters['split_on_hr'] = split_on_hr +# ------------------------------------------------ END templates setup ------------------------------------------------------ -def tag_id_of_name(tag): - return tag.strip().replace(' ', '-') -env.globals['tag_id_of_name'] = tag_id_of_name -env.globals['tag_ids_of_names'] = lambda ns: ' '.join(tag_id_of_name(n) for n in ns) -def write_pure_md_file(source, dest, name, loc_map): +# ------------------------------------------------ START write destination files ---------------------------------------------- + +def open_outfile(filename, mode = 'w'): + filename = os.path.join(MATHLIB_DEST_ROOT, filename) + os.makedirs(os.path.dirname(filename), exist_ok=True) + return open(filename, mode, encoding='utf-8') + +def write_pure_md_file(source, dest, name): with open(source) as infile: body = convert_markdown(infile.read(), True) @@ -384,44 +354,6 @@ def write_pure_md_file(source, dest, name, loc_map): body = body, )) -def mk_site_tree(partition: List[ImportName]): - filenames = [ [filename.project] + list(filename.parts) for filename in partition ] - return mk_site_tree_core(filenames) - -def mk_site_tree_core(filenames, path=[]): - entries = [] - - for dirname in sorted(set(dirname for dirname, *rest in filenames if rest != [])): - new_path = path + [dirname] - entries.append({ - "kind": "project" if not path else "dir", - "name": dirname, - "path": '/'.join(new_path[1:]), - "children": mk_site_tree_core([rest for dn, *rest in filenames if rest != [] and dn == dirname], new_path) - }) - - for filename in sorted(filename for filename, *rest in filenames if rest == []): - new_path = path + [filename] - entries.append({ - "kind": "file", - "name": filename, - "path": '/'.join(new_path[1:]) + '.html', - }) - - return entries - -def setup_jinja_globals(file_map, loc_map, instances): - env.globals['import_graph'] = trace_deps(file_map) - env.globals['site_tree'] = mk_site_tree(file_map) - env.globals['instances'] = instances - env.globals['import_options'] = lambda d, i: import_options(loc_map, d, i) - env.globals['find_import_path'] = lambda d: find_import_path(loc_map, d) - env.filters['linkify'] = lambda x: linkify(x, loc_map) - env.filters['linkify_efmt'] = lambda x: linkify_efmt(x, loc_map) - env.filters['convert_markdown'] = lambda x: linkify_markdown(convert_markdown(x), loc_map) # TODO: this is probably very broken - env.filters['link_to_decl'] = lambda x: link_to_decl(x, loc_map) - env.filters['plaintext_summary'] = lambda x: plaintext_summary(x) - def write_html_files(partition, loc_map, notes, mod_docs, instances, tactic_docs): with open_outfile('index.html') as out: out.write(env.get_template('index.j2').render( @@ -447,7 +379,7 @@ def write_html_files(partition, loc_map, notes, mod_docs, instances, tactic_docs for filename, decls in partition.items(): md = mod_docs.get(filename, []) - with open_outfile(html_root + filename.url) as out: + with open_outfile(MATHLIB_DEST_ROOT + filename.url) as out: out.write(env.get_template('module.j2').render( active_path = filename.url, filename = filename, @@ -455,20 +387,40 @@ def write_html_files(partition, loc_map, notes, mod_docs, instances, tactic_docs decl_names = sorted(d['name'] for d in decls), )) - for (filename, displayname, source, _) in extra_doc_files: - write_pure_md_file(local_lean_root + source, filename + '.html', displayname, loc_map) + for (filename, displayname, source, _) in EXTRA_DOC_FILES: + write_pure_md_file(MATHLIB_SRC_ROOT + source, filename + '.html', displayname) def write_site_map(partition): with open_outfile('sitemap.txt') as out: for filename in partition: - out.write(site_root + filename.url + '\n') + out.write(SITE_ROOT + filename.url + '\n') for n in ['index', 'tactics', 'commands', 'hole_commands', 'notes']: - out.write(site_root + n + '.html\n') - for (filename, _, _, _) in extra_doc_files: - out.write(site_root + filename + '.html\n') + out.write(SITE_ROOT + n + '.html\n') + for (filename, _, _, _) in EXTRA_DOC_FILES: + out.write(SITE_ROOT + filename + '.html\n') + +def name_in_decl(decl_name, dmap): + if dmap['name'] == decl_name: + return True + if decl_name in [sf[0] for sf in dmap['structure_fields']]: + return True + if decl_name in [sf[0] for sf in dmap['constructors']]: + return True + return False + +def library_link_from_decl_name(decl_name, decl_loc, file_map): + try: + e = next(d for d in file_map[decl_loc] if name_in_decl(decl_name, d)) + except StopIteration as e: + if decl_name[-3:] == '.mk': + return library_link_from_decl_name(decl_name[:-3], decl_loc, file_map) + print(f'{decl_name} appears in {decl_loc}, but we do not have data for that declaration. file_map:') + print(file_map[decl_loc]) + raise e + return library_link(decl_loc, e['line']) def write_docs_redirect(decl_name, decl_loc): - url = site_root + decl_loc.url + url = SITE_ROOT + decl_loc.url with open_outfile('find/' + decl_name + '/index.html') as out: out.write(f'') @@ -477,6 +429,7 @@ def write_src_redirect(decl_name, decl_loc, file_map): with open_outfile('find/' + decl_name + '/src/index.html') as out: out.write(f'') +# TODO: see if we can do without the 'find' dir def write_redirects(loc_map, file_map): for decl_name in loc_map: if decl_name.startswith('con.') and sys.platform == 'win32': @@ -484,7 +437,7 @@ def write_redirects(loc_map, file_map): write_docs_redirect(decl_name, loc_map[decl_name]) write_src_redirect(decl_name, loc_map[decl_name], file_map) -def copy_css(path, use_symlinks): +def copy_web_files(path, use_symlinks): def cp(a, b): if use_symlinks: try: @@ -501,54 +454,63 @@ def cp(a, b): cp('searchWorker.js', path+'searchWorker.js') def copy_yaml_files(path): - for fn in ['100.yaml', 'undergrad.yaml', 'overview.yaml']: - shutil.copyfile(f'{local_lean_root}docs/{fn}', path+fn) + for name in ['100.yaml', 'undergrad.yaml', 'overview.yaml']: + shutil.copyfile(f'{MATHLIB_SRC_ROOT}docs/{name}', path+name) def copy_static_files(path): - for filename in glob.glob(os.path.join(root, 'static', '*.*')): + for filename in glob.glob(os.path.join(ROOT, 'static', '*.*')): shutil.copy(filename, path) +def copy_files(path, use_symlinks): + copy_web_files(path, use_symlinks) + copy_yaml_files(path) + copy_static_files(path) + +# write only declaration names in separate file +# TODO: delete when using data structure for searching def write_decl_txt(loc_map): with open_outfile('decl.txt') as out: out.write('\n'.join(loc_map.keys())) -def mk_export_map_entry(decl_name, filename, kind, is_meta, line, args, tp): - return {'filename': str(filename.raw_path), - 'kind': kind, - 'is_meta': is_meta, - 'line': line, - # 'args': args, - # 'type': tp, - 'src_link': library_link(filename, line), - 'docs_link': f'{site_root}{filename.url}#{decl_name}'} - -def mk_export_db(loc_map, file_map): +def mk_export_map_entry(decl_name, filename, kind, is_meta, line): + return { + 'filename': str(filename.raw_path), + 'kind': kind, + 'is_meta': is_meta, + 'line': line, + 'src_link': library_link(filename, line), + 'docs_link': f'{SITE_ROOT}{filename.url}#{decl_name}' + } + +def mk_export_db(file_map): export_db = {} for _, decls in file_map.items(): for obj in decls: - export_db[obj['name']] = mk_export_map_entry(obj['name'], obj['filename'], obj['kind'], obj['is_meta'], obj['line'], obj['args'], obj['type']) + export_db[obj['name']] = mk_export_map_entry(obj['name'], obj['filename'], obj['kind'], obj['is_meta'], obj['line']) export_db[obj['name']]['decl_header_html'] = env.get_template('decl_header.j2').render(decl=obj) - for (cstr_name, tp) in obj['constructors']: - export_db[cstr_name] = mk_export_map_entry(cstr_name, obj['filename'], obj['kind'], obj['is_meta'], obj['line'], [], tp) - for (sf_name, tp) in obj['structure_fields']: - export_db[sf_name] = mk_export_map_entry(sf_name, obj['filename'], obj['kind'], obj['is_meta'], obj['line'], [], tp) + for (cstr_name, _) in obj['constructors']: + export_db[cstr_name] = mk_export_map_entry(cstr_name, obj['filename'], obj['kind'], obj['is_meta'], obj['line']) + for (sf_name, _) in obj['structure_fields']: + export_db[sf_name] = mk_export_map_entry(sf_name, obj['filename'], obj['kind'], obj['is_meta'], obj['line']) return export_db def write_export_db(export_db): json_str = json.dumps(export_db) - with gzip.GzipFile(html_root + 'export_db.json.gz', 'w') as zout: + with gzip.GzipFile(MATHLIB_DEST_ROOT + 'export_db.json.gz', 'w') as zout: zout.write(json_str.encode('utf-8')) +# ------------------------------------------------ END write destination files ---------------------------------------------- + def main(): - file_map, loc_map, notes, mod_docs, instances, tactic_docs = load_json() - setup_jinja_globals(file_map, loc_map, instances) + file_map, loc_map, notes, mod_docs, instances, tactic_docs = read_src_data() + + setup_jinja_env(file_map, loc_map, instances) write_decl_txt(loc_map) write_html_files(file_map, loc_map, notes, mod_docs, instances, tactic_docs) + write_redirects(loc_map, file_map) - copy_css(html_root, use_symlinks=cl_args.l) - copy_yaml_files(html_root) - copy_static_files(html_root) - write_export_db(mk_export_db(loc_map, file_map)) + copy_files(MATHLIB_DEST_ROOT, use_symlinks=CLI_ARGS.l) + write_export_db(mk_export_db(file_map)) write_site_map(file_map) if __name__ == '__main__': From 7110fa7566fda295bc2c6c9fa95b4756e49327c6 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Thu, 21 Jan 2021 17:33:53 +0200 Subject: [PATCH 05/25] extract data structures for readability --- mathlib_data_structures.py | 60 +++++++++++++++++++ print_docs.py | 118 ++++++++++++++++++++++--------------- 2 files changed, 131 insertions(+), 47 deletions(-) create mode 100644 mathlib_data_structures.py diff --git a/mathlib_data_structures.py b/mathlib_data_structures.py new file mode 100644 index 0000000..3f09de0 --- /dev/null +++ b/mathlib_data_structures.py @@ -0,0 +1,60 @@ +mathlibStructures = dict( + DECLARATIONS = 'decl', + TACTICS = 'tactic_docs', + MODULE_DESCRIPTIONS = 'mod_docs', + NOTES = 'notes', + INSTANCES = 'instances' +) + +declaration = dict( + NAME = 'name', + IS_META = 'is_meta', + ARGS = 'args', + TYPE = 'type', + DOC_STRING = 'doc_string', + FILENAME = 'filename', + LINE = 'line', + ATTRIBUTES = 'attributes', + EQUATIONS = 'equations', + KIND = 'kind', + STRUCTURE_FIELDS = 'structure_fields', + CONSTRUCTORS = 'constructors' +) + +declarationKindsSource = dict( + THEOREM = 'thm', + CONST = 'cnst', + AXIOM = 'ax' +) + +declarationKindsDestination = dict( + STRUCTURE = 'structure', + INDUCTIVE = 'inductive', + THEOREM = 'theorem', + CONST = 'const', + AXIOM = 'axiom' +) + +tactic = dict( + NAME = 'name', + CATEGORY = 'category', + DECL_NAMES = 'decl_names', + TAGS = 'tags', + DESCRIPTION = 'description', + IMPORT = 'import' +) + +tacticCategories = dict( + TACTIC = 'tactic', + COMMAND = 'command', + HOLE_COMMAND = 'hole_command', + ATTRIBUTE = 'attribute' +) + +generalPages = dict( + INDEX = 'index', + TACTICS = 'tactics', + COMMANDS = 'commands', + HOLE_COMMANDS = 'hole_commands', + ATTRIBUTES = 'notes', +) \ No newline at end of file diff --git a/print_docs.py b/print_docs.py index 35d62cc..b46f3f5 100644 --- a/print_docs.py +++ b/print_docs.py @@ -21,6 +21,7 @@ from typing import List from collections import defaultdict from import_name import ImportName +from mathlib_data_structures import mathlibStructures, declaration, tactic, tacticCategories, declarationKindsSource, declarationKindsDestination, generalPages # data structures manipulation import json @@ -33,6 +34,7 @@ from urllib.parse import quote from functools import reduce import networkx as nx +from operator import itemgetter # get arguments from script inititation parser = argparse.ArgumentParser('Options to print_docs.py') @@ -86,18 +88,18 @@ def separate_results(objs): loc_map = {} for obj in objs: # replace the filenames in-place with parsed filename objects - i_name = obj['filename'] = ImportName.of(obj['filename']) + i_name = obj[declaration['FILENAME']] = ImportName.of(obj[declaration['FILENAME']]) if i_name.project == '.': continue # this is doc-gen itself file_map[i_name].append(obj) - loc_map[obj['name']] = i_name - for (cstr_name, _) in obj['constructors']: + loc_map[obj[declaration['NAME']]] = i_name + for (cstr_name, _) in obj[declaration['CONSTRUCTORS']]: loc_map[cstr_name] = i_name - for (sf_name, _) in obj['structure_fields']: + for (sf_name, _) in obj[declaration['STRUCTURE_FIELDS']]: loc_map[sf_name] = i_name - if len(obj['structure_fields']) > 0: - loc_map[obj['name'] + '.mk'] = i_name + if len(obj[declaration['STRUCTURE_FIELDS']]) > 0: + loc_map[obj[declaration['NAME']] + '.mk'] = i_name return file_map, loc_map # ------------------------------------------------ END utils reading --------------------------------------------------- @@ -107,20 +109,22 @@ def separate_results(objs): def read_src_data(): with open('export.json', 'r', encoding='utf-8') as f: - decls = json.load(f, strict=False) - file_map, loc_map = separate_results(decls['decls']) - for entry in decls['tactic_docs']: - if len(entry['tags']) == 0: - entry['tags'] = ['untagged'] + lib_data = json.load(f, strict=False) - mod_docs = {ImportName.of(f): docs for f, docs in decls['mod_docs'].items()} + file_map, loc_map = separate_results(lib_data[mathlibStructures['DECLARATIONS']]) + + for entry in lib_data[mathlibStructures['TACTICS']]: + if len(entry[tactic['TAGS']]) == 0: + entry[tactic['TAGS']] = ['untagged'] + + mod_docs = {ImportName.of(f): docs for f, docs in lib_data[mathlibStructures['MODULE_DESCRIPTIONS']].items()} # ensure the key is present for `default.lean` modules with no declarations for i_name in mod_docs: if i_name.project == '.': continue # this is doc-gen itself file_map[i_name] - return file_map, loc_map, decls['notes'], mod_docs, decls['instances'], decls['tactic_docs'] + return file_map, loc_map, lib_data[mathlibStructures['NOTES']], mod_docs, lib_data[mathlibStructures['INSTANCES']], lib_data[mathlibStructures['TACTICS']] # ------------------------------------------------ END read source files ----------------------------------------------------- @@ -160,8 +164,8 @@ def trace_deps(file_map): print(f"trace_deps: Processed {n_ok} / {n} dependency links") return graph -def mk_site_tree(partition: List[ImportName]): - filenames = [ [filename.project] + list(filename.parts) for filename in partition ] +def mk_site_tree(file_map: List[ImportName]): + filenames = [ [filename.project] + list(filename.parts) for filename in file_map ] return mk_site_tree_core(filenames) def mk_site_tree_core(filenames, path=[]): @@ -201,11 +205,16 @@ def import_options(loc_map, decl_name, import_string): return '' def kind_of_decl(decl): - kind = 'structure' if len(decl['structure_fields']) > 0 else 'inductive' if len(decl['constructors']) > 0 else decl['kind'] - if kind == 'thm': kind = 'theorem' - elif kind == 'cnst': kind = 'constant' - elif kind == 'ax': kind = 'axiom' - return kind + if len(decl[declaration['STRUCTURE_FIELDS']]) > 0: + return declarationKindsDestination['STRUCTURE'] + elif len(decl[declaration['CONSTRUCTORS']]) > 0: + return declarationKindsDestination['INDUCTIVE'] + elif decl[declaration['KIND']] == declarationKindsSource['THEOREM']: + return declarationKindsDestination['THEOREM'] + elif decl[declaration['KIND']] == declarationKindsSource['CONSTANT']: + return declarationKindsDestination['CONSTANT'] + elif decl[declaration['KIND']] == declarationKindsSource['AXIOM']: + return declarationKindsDestination['AXIOM'] def tag_id_of_name(tag): return tag.strip().replace(' ', '-') @@ -354,7 +363,7 @@ def write_pure_md_file(source, dest, name): body = body, )) -def write_html_files(partition, loc_map, notes, mod_docs, instances, tactic_docs): +def write_html_files(file_map, notes, mod_docs, tactic_docs): with open_outfile('index.html') as out: out.write(env.get_template('index.j2').render( active_path='')) @@ -368,56 +377,62 @@ def write_html_files(partition, loc_map, notes, mod_docs, instances, tactic_docs active_path='', notes = sorted(notes, key = lambda n: n[0]))) - kinds = [('tactic', 'tactics'), ('command', 'commands'), ('hole_command', 'hole_commands'), ('attribute', 'attributes')] - for (kind, filename) in kinds: - entries = [e for e in tactic_docs if e['category'] == kind] + types_of_tactics = [ + (tacticCategories['TACTIC'], generalPages['TACTICS']), + (tacticCategories['COMMAND'], generalPages['COMMANDS']), + (tacticCategories['HOLE_COMMAND'], generalPages['HOLE_COMMANDS']), + (tacticCategories['ATTRIBUTE'], generalPages['ATTRIBUTES']) + ] + for (category, filename) in types_of_tactics: + entries = [e for e in tactic_docs if e[tactic['CATEGORY']] == category] with open_outfile(filename + '.html') as out: out.write(env.get_template(filename + '.j2').render( active_path='', - entries = sorted(entries, key = lambda n: n['name']), - tagset = sorted(set(t for e in entries for t in e['tags'])))) + entries = sorted(entries, key = lambda n: n[tactic['NAME']]), + tagset = sorted(set(t for e in entries for t in e[tactic['TAGS']])) + )) - for filename, decls in partition.items(): + for filename, decls in file_map.items(): md = mod_docs.get(filename, []) with open_outfile(MATHLIB_DEST_ROOT + filename.url) as out: out.write(env.get_template('module.j2').render( active_path = filename.url, filename = filename, - items = sorted(md + decls, key = lambda d: d['line']), - decl_names = sorted(d['name'] for d in decls), + items = sorted(md + decls, key = lambda d: d[declaration['LINE']]), + decl_names = sorted(d[declaration['NAME']] for d in decls), )) for (filename, displayname, source, _) in EXTRA_DOC_FILES: write_pure_md_file(MATHLIB_SRC_ROOT + source, filename + '.html', displayname) -def write_site_map(partition): +def write_site_map(file_map): with open_outfile('sitemap.txt') as out: - for filename in partition: + for filename in file_map: out.write(SITE_ROOT + filename.url + '\n') - for n in ['index', 'tactics', 'commands', 'hole_commands', 'notes']: - out.write(SITE_ROOT + n + '.html\n') + for name in generalPages.values(): + out.write(SITE_ROOT + name + '.html\n') for (filename, _, _, _) in EXTRA_DOC_FILES: out.write(SITE_ROOT + filename + '.html\n') -def name_in_decl(decl_name, dmap): - if dmap['name'] == decl_name: +def name_in_decl(decl_name, decl): + if decl[declaration['NAME']] == decl_name: return True - if decl_name in [sf[0] for sf in dmap['structure_fields']]: + if decl_name in [sf[0] for sf in decl[declaration['STRUCTURE_FIELDS']]]: return True - if decl_name in [sf[0] for sf in dmap['constructors']]: + if decl_name in [cnstr[0] for cnstr in decl[declaration['CONSTRUCTORS']]]: return True return False def library_link_from_decl_name(decl_name, decl_loc, file_map): try: - e = next(d for d in file_map[decl_loc] if name_in_decl(decl_name, d)) + e = next(decl for decl in file_map[decl_loc] if name_in_decl(decl_name, decl)) except StopIteration as e: if decl_name[-3:] == '.mk': return library_link_from_decl_name(decl_name[:-3], decl_loc, file_map) print(f'{decl_name} appears in {decl_loc}, but we do not have data for that declaration. file_map:') print(file_map[decl_loc]) raise e - return library_link(decl_loc, e['line']) + return library_link(decl_loc, e[declaration['LINE']]) def write_docs_redirect(decl_name, decl_loc): url = SITE_ROOT + decl_loc.url @@ -484,14 +499,23 @@ def mk_export_map_entry(decl_name, filename, kind, is_meta, line): def mk_export_db(file_map): export_db = {} - for _, decls in file_map.items(): + for decls in file_map.values(): for obj in decls: - export_db[obj['name']] = mk_export_map_entry(obj['name'], obj['filename'], obj['kind'], obj['is_meta'], obj['line']) - export_db[obj['name']]['decl_header_html'] = env.get_template('decl_header.j2').render(decl=obj) - for (cstr_name, _) in obj['constructors']: - export_db[cstr_name] = mk_export_map_entry(cstr_name, obj['filename'], obj['kind'], obj['is_meta'], obj['line']) - for (sf_name, _) in obj['structure_fields']: - export_db[sf_name] = mk_export_map_entry(sf_name, obj['filename'], obj['kind'], obj['is_meta'], obj['line']) + name, filename, kind, is_meta, line, constructors, structure_fields = itemgetter( + declaration['NAME'], + declaration['FILENAME'], + declaration['KIND'], + declaration['IS_META'], + declaration['LINE'], + declaration['CONSTRUCTORS'], + declaration['STRUCTURE_FIELDS'] + )(obj) + export_db[name] = mk_export_map_entry(name, filename, kind, is_meta, line) + export_db[name]['decl_header_html'] = env.get_template('decl_header.j2').render(decl=obj) + for (cstr_name, _) in constructors: + export_db[cstr_name] = mk_export_map_entry(cstr_name, filename, kind, is_meta, line) + for (sf_name, _) in structure_fields: + export_db[sf_name] = mk_export_map_entry(sf_name, filename, kind, is_meta, line) return export_db def write_export_db(export_db): @@ -506,7 +530,7 @@ def main(): setup_jinja_env(file_map, loc_map, instances) write_decl_txt(loc_map) - write_html_files(file_map, loc_map, notes, mod_docs, instances, tactic_docs) + write_html_files(file_map, notes, mod_docs, tactic_docs) write_redirects(loc_map, file_map) copy_files(MATHLIB_DEST_ROOT, use_symlinks=CLI_ARGS.l) From ab0e46f221ab81ded19464ab2507783886610385 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Thu, 21 Jan 2021 18:10:56 +0100 Subject: [PATCH 06/25] fix build --- mathlib_data_structures.py | 2 +- print_docs.py | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/mathlib_data_structures.py b/mathlib_data_structures.py index 3f09de0..2936f17 100644 --- a/mathlib_data_structures.py +++ b/mathlib_data_structures.py @@ -1,5 +1,5 @@ mathlibStructures = dict( - DECLARATIONS = 'decl', + DECLARATIONS = 'decls', TACTICS = 'tactic_docs', MODULE_DESCRIPTIONS = 'mod_docs', NOTES = 'notes', diff --git a/print_docs.py b/print_docs.py index b46f3f5..b88ef30 100644 --- a/print_docs.py +++ b/print_docs.py @@ -211,8 +211,8 @@ def kind_of_decl(decl): return declarationKindsDestination['INDUCTIVE'] elif decl[declaration['KIND']] == declarationKindsSource['THEOREM']: return declarationKindsDestination['THEOREM'] - elif decl[declaration['KIND']] == declarationKindsSource['CONSTANT']: - return declarationKindsDestination['CONSTANT'] + elif decl[declaration['KIND']] == declarationKindsSource['CONST']: + return declarationKindsDestination['CONST'] elif decl[declaration['KIND']] == declarationKindsSource['AXIOM']: return declarationKindsDestination['AXIOM'] From 67b7951094ef3021a3f35b0187f549461dcef820 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Thu, 21 Jan 2021 18:27:48 +0100 Subject: [PATCH 07/25] use class instead of dict for structure field names This way pylint will notice if you accidentally use the wrong key. I'm not sure if this is officially "pythonic". It seems like more could be done translating the json to actual data structures with named fields; then these lookup tables wouldn't be necessary! But this might be a lot of work for little gain. --- mathlib_data_structures.py | 15 ++++++++------- print_docs.py | 8 ++++---- 2 files changed, 12 insertions(+), 11 deletions(-) diff --git a/mathlib_data_structures.py b/mathlib_data_structures.py index 2936f17..16c4ac4 100644 --- a/mathlib_data_structures.py +++ b/mathlib_data_structures.py @@ -1,10 +1,9 @@ -mathlibStructures = dict( - DECLARATIONS = 'decls', - TACTICS = 'tactic_docs', - MODULE_DESCRIPTIONS = 'mod_docs', - NOTES = 'notes', +class mathlibStructures: + DECLARATIONS = 'decls' + TACTICS = 'tactic_docs' + MODULE_DESCRIPTIONS = 'mod_docs' + NOTES = 'notes' INSTANCES = 'instances' -) declaration = dict( NAME = 'name', @@ -57,4 +56,6 @@ COMMANDS = 'commands', HOLE_COMMANDS = 'hole_commands', ATTRIBUTES = 'notes', -) \ No newline at end of file +) + + diff --git a/print_docs.py b/print_docs.py index b88ef30..ec03fc3 100644 --- a/print_docs.py +++ b/print_docs.py @@ -111,20 +111,20 @@ def read_src_data(): with open('export.json', 'r', encoding='utf-8') as f: lib_data = json.load(f, strict=False) - file_map, loc_map = separate_results(lib_data[mathlibStructures['DECLARATIONS']]) + file_map, loc_map = separate_results(lib_data[mathlibStructures.DECLARATIONS]) - for entry in lib_data[mathlibStructures['TACTICS']]: + for entry in lib_data[mathlibStructures.TACTICS]: if len(entry[tactic['TAGS']]) == 0: entry[tactic['TAGS']] = ['untagged'] - mod_docs = {ImportName.of(f): docs for f, docs in lib_data[mathlibStructures['MODULE_DESCRIPTIONS']].items()} + mod_docs = {ImportName.of(f): docs for f, docs in lib_data[mathlibStructures.MODULE_DESCRIPTIONS].items()} # ensure the key is present for `default.lean` modules with no declarations for i_name in mod_docs: if i_name.project == '.': continue # this is doc-gen itself file_map[i_name] - return file_map, loc_map, lib_data[mathlibStructures['NOTES']], mod_docs, lib_data[mathlibStructures['INSTANCES']], lib_data[mathlibStructures['TACTICS']] + return file_map, loc_map, lib_data[mathlibStructures.NOTES], mod_docs, lib_data[mathlibStructures.INSTANCES], lib_data[mathlibStructures.TACTICS] # ------------------------------------------------ END read source files ----------------------------------------------------- From d965133c0ee99ce6ed39ada153f70ca8030db93c Mon Sep 17 00:00:00 2001 From: polibb Date: Sun, 7 Feb 2021 11:19:26 +0200 Subject: [PATCH 08/25] small fixes --- leanpkg.toml | 4 +- mathlib_data_structures.py | 91 ++++++++++++++++++++------------------ nav.js | 4 +- 3 files changed, 51 insertions(+), 48 deletions(-) diff --git a/leanpkg.toml b/leanpkg.toml index c29fc17..d70935b 100644 --- a/leanpkg.toml +++ b/leanpkg.toml @@ -1,8 +1,8 @@ [package] name = "." version = "0.1" -lean_version = "leanprover-community/lean:3.23.0" +lean_version = "leanprover-community/lean:3.24.0" path = "src" [dependencies] -mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "5a61ef1981738b829ff712cab18e63a675108c40"} \ No newline at end of file +mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "aa744dba88de45c7b91ca81b1bb526e7e312d7e1"} diff --git a/mathlib_data_structures.py b/mathlib_data_structures.py index 16c4ac4..92eb51e 100644 --- a/mathlib_data_structures.py +++ b/mathlib_data_structures.py @@ -1,3 +1,6 @@ +from dataclasses import dataclass, field + +@dataclass class mathlibStructures: DECLARATIONS = 'decls' TACTICS = 'tactic_docs' @@ -5,57 +8,57 @@ class mathlibStructures: NOTES = 'notes' INSTANCES = 'instances' -declaration = dict( - NAME = 'name', - IS_META = 'is_meta', - ARGS = 'args', - TYPE = 'type', - DOC_STRING = 'doc_string', - FILENAME = 'filename', - LINE = 'line', - ATTRIBUTES = 'attributes', - EQUATIONS = 'equations', - KIND = 'kind', - STRUCTURE_FIELDS = 'structure_fields', +@dataclass +class declaration: + NAME = 'name' + IS_META = 'is_meta' + ARGS = 'args' + TYPE = 'type' + DOC_STRING = 'doc_string' + FILENAME = 'filename' + LINE = 'line' + ATTRIBUTES = 'attributes' + EQUATIONS = 'equations' + KIND = 'kind' + STRUCTURE_FIELDS = 'structure_fields' CONSTRUCTORS = 'constructors' -) -declarationKindsSource = dict( - THEOREM = 'thm', - CONST = 'cnst', +@dataclass +class declarationKindsSource: + THEOREM = 'thm' + CONST = 'cnst' AXIOM = 'ax' -) -declarationKindsDestination = dict( - STRUCTURE = 'structure', - INDUCTIVE = 'inductive', - THEOREM = 'theorem', - CONST = 'const', +@dataclass +class declarationKindsDestination: + STRUCTURE = 'structure' + INDUCTIVE = 'inductive' + THEOREM = 'theorem' + CONST = 'const' AXIOM = 'axiom' -) - -tactic = dict( - NAME = 'name', - CATEGORY = 'category', - DECL_NAMES = 'decl_names', - TAGS = 'tags', - DESCRIPTION = 'description', + +@dataclass +class tactic: + NAME = 'name' + CATEGORY = 'category' + DECL_NAMES = 'decl_names' + TAGS = 'tags' + DESCRIPTION = 'description' IMPORT = 'import' -) -tacticCategories = dict( - TACTIC = 'tactic', - COMMAND = 'command', - HOLE_COMMAND = 'hole_command', +@dataclass +class tacticCategories: + TACTIC = 'tactic' + COMMAND = 'command' + HOLE_COMMAND = 'hole_command' ATTRIBUTE = 'attribute' -) - -generalPages = dict( - INDEX = 'index', - TACTICS = 'tactics', - COMMANDS = 'commands', - HOLE_COMMANDS = 'hole_commands', - ATTRIBUTES = 'notes', -) + +@dataclass +class generalPages: + INDEX = 'index' + TACTICS = 'tactics' + COMMANDS = 'commands' + HOLE_COMMANDS = 'hole_commands' + ATTRIBUTES = 'notes' diff --git a/nav.js b/nav.js index 6d39d94..efdec8e 100644 --- a/nav.js +++ b/nav.js @@ -168,7 +168,7 @@ searchInputElmnt.addEventListener('input', async (ev) => { const d = resultsElmntCopy.appendChild(document.createElement('a')); d.innerText = decl; d.title = decl; - d.href = `${siteRoot}find/${decl}`; // todo why not a link directly to the declaration in docs? + d.href = `${siteRoot}find/${decl}`; } resultsElmntCopy.setAttribute('state', 'done'); currentResultsElmnt.replaceWith(resultsElmntCopy); @@ -193,7 +193,7 @@ if (suggestionsElmnt) { for (const { decl } of results) { const li = ul.appendChild(document.createElement('li')); const a = li.appendChild(document.createElement('a')); - a.href = `${siteRoot}find/${decl}`; // todo why not a link directly? + a.href = `${siteRoot}find/${decl}`; a.appendChild(document.createElement('code')).innerText = decl; } }); From ac59932eeff5bc31ade8ec13d01b507ce431f6cb Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Wed, 10 Feb 2021 11:07:40 +0200 Subject: [PATCH 09/25] main py script structure fixes --- mathlib_data_structures.py | 80 ++++++++++++++++------------------- print_docs.py | 87 +++++++++++++++++++------------------- 2 files changed, 79 insertions(+), 88 deletions(-) diff --git a/mathlib_data_structures.py b/mathlib_data_structures.py index 16c4ac4..e296906 100644 --- a/mathlib_data_structures.py +++ b/mathlib_data_structures.py @@ -5,57 +5,49 @@ class mathlibStructures: NOTES = 'notes' INSTANCES = 'instances' -declaration = dict( - NAME = 'name', - IS_META = 'is_meta', - ARGS = 'args', - TYPE = 'type', - DOC_STRING = 'doc_string', - FILENAME = 'filename', - LINE = 'line', - ATTRIBUTES = 'attributes', - EQUATIONS = 'equations', - KIND = 'kind', - STRUCTURE_FIELDS = 'structure_fields', +class declaration: + NAME = 'name' + IS_META = 'is_meta' + ARGS = 'args' + TYPE = 'type' + DOC_STRING = 'doc_string' + FILENAME = 'filename' + LINE = 'line' + ATTRIBUTES = 'attributes' + EQUATIONS = 'equations' + KIND = 'kind' + STRUCTURE_FIELDS = 'structure_fields' CONSTRUCTORS = 'constructors' -) -declarationKindsSource = dict( - THEOREM = 'thm', - CONST = 'cnst', +class declarationKindsSource: + THEOREM = 'thm' + CONST = 'cnst' AXIOM = 'ax' -) -declarationKindsDestination = dict( - STRUCTURE = 'structure', - INDUCTIVE = 'inductive', - THEOREM = 'theorem', - CONST = 'const', +class declarationKindsDestination: + STRUCTURE = 'structure' + INDUCTIVE = 'inductive' + THEOREM = 'theorem' + CONST = 'const' AXIOM = 'axiom' -) -tactic = dict( - NAME = 'name', - CATEGORY = 'category', - DECL_NAMES = 'decl_names', - TAGS = 'tags', - DESCRIPTION = 'description', +class tactic: + NAME = 'name' + CATEGORY = 'category' + DECL_NAMES = 'decl_names' + TAGS = 'tags' + DESCRIPTION = 'description' IMPORT = 'import' -) -tacticCategories = dict( - TACTIC = 'tactic', - COMMAND = 'command', - HOLE_COMMAND = 'hole_command', +class tacticCategories: + TACTIC = 'tactic' + COMMAND = 'command' + HOLE_COMMAND = 'hole_command' ATTRIBUTE = 'attribute' -) - -generalPages = dict( - INDEX = 'index', - TACTICS = 'tactics', - COMMANDS = 'commands', - HOLE_COMMANDS = 'hole_commands', - ATTRIBUTES = 'notes', -) - +class generalPages: + INDEX = 'index' + TACTICS = 'tactics' + COMMANDS = 'commands' + HOLE_COMMANDS = 'hole_commands' + ATTRIBUTES = 'notes' \ No newline at end of file diff --git a/print_docs.py b/print_docs.py index ec03fc3..5ad1be5 100644 --- a/print_docs.py +++ b/print_docs.py @@ -88,18 +88,18 @@ def separate_results(objs): loc_map = {} for obj in objs: # replace the filenames in-place with parsed filename objects - i_name = obj[declaration['FILENAME']] = ImportName.of(obj[declaration['FILENAME']]) + i_name = obj[declaration.FILENAME] = ImportName.of(obj[declaration.FILENAME]) if i_name.project == '.': continue # this is doc-gen itself file_map[i_name].append(obj) - loc_map[obj[declaration['NAME']]] = i_name - for (cstr_name, _) in obj[declaration['CONSTRUCTORS']]: + loc_map[obj[declaration.NAME]] = i_name + for (cstr_name, _) in obj[declaration.CONSTRUCTORS]: loc_map[cstr_name] = i_name - for (sf_name, _) in obj[declaration['STRUCTURE_FIELDS']]: + for (sf_name, _) in obj[declaration.STRUCTURE_FIELDS]: loc_map[sf_name] = i_name - if len(obj[declaration['STRUCTURE_FIELDS']]) > 0: - loc_map[obj[declaration['NAME']] + '.mk'] = i_name + if len(obj[declaration.STRUCTURE_FIELDS]) > 0: + loc_map[obj[declaration.NAME] + '.mk'] = i_name return file_map, loc_map # ------------------------------------------------ END utils reading --------------------------------------------------- @@ -114,8 +114,8 @@ def read_src_data(): file_map, loc_map = separate_results(lib_data[mathlibStructures.DECLARATIONS]) for entry in lib_data[mathlibStructures.TACTICS]: - if len(entry[tactic['TAGS']]) == 0: - entry[tactic['TAGS']] = ['untagged'] + if len(entry[tactic.TAGS]) == 0: + entry[tactic.TAGS] = ['untagged'] mod_docs = {ImportName.of(f): docs for f, docs in lib_data[mathlibStructures.MODULE_DESCRIPTIONS].items()} # ensure the key is present for `default.lean` modules with no declarations @@ -157,7 +157,7 @@ def trace_deps(file_map): try: p = import_name_by_path[Path(p).with_suffix('.lean')] except KeyError: - print(f"trace_deps: Path not recognized: {p}") + print(f"trace_deps: Path does not end in 'lean': {p}") continue graph.add_edge(k, p) n_ok += 1 @@ -205,16 +205,16 @@ def import_options(loc_map, decl_name, import_string): return '' def kind_of_decl(decl): - if len(decl[declaration['STRUCTURE_FIELDS']]) > 0: - return declarationKindsDestination['STRUCTURE'] - elif len(decl[declaration['CONSTRUCTORS']]) > 0: - return declarationKindsDestination['INDUCTIVE'] - elif decl[declaration['KIND']] == declarationKindsSource['THEOREM']: - return declarationKindsDestination['THEOREM'] - elif decl[declaration['KIND']] == declarationKindsSource['CONST']: - return declarationKindsDestination['CONST'] - elif decl[declaration['KIND']] == declarationKindsSource['AXIOM']: - return declarationKindsDestination['AXIOM'] + if len(decl[declaration.STRUCTURE_FIELDS]) > 0: + return declarationKindsDestination.STRUCTURE + elif len(decl[declaration.CONSTRUCTORS]) > 0: + return declarationKindsDestination.INDUCTIVE + elif decl[declaration.KIND] == declarationKindsSource.THEOREM: + return declarationKindsDestination.THEOREM + elif decl[declaration.KIND] == declarationKindsSource.CONST: + return declarationKindsDestination.CONST + elif decl[declaration.KIND] == declarationKindsSource.AXIOM: + return declarationKindsDestination.AXIOM def tag_id_of_name(tag): return tag.strip().replace(' ', '-') @@ -378,18 +378,18 @@ def write_html_files(file_map, notes, mod_docs, tactic_docs): notes = sorted(notes, key = lambda n: n[0]))) types_of_tactics = [ - (tacticCategories['TACTIC'], generalPages['TACTICS']), - (tacticCategories['COMMAND'], generalPages['COMMANDS']), - (tacticCategories['HOLE_COMMAND'], generalPages['HOLE_COMMANDS']), - (tacticCategories['ATTRIBUTE'], generalPages['ATTRIBUTES']) + (tacticCategories.TACTIC, generalPages.TACTICS), + (tacticCategories.COMMAND, generalPages.COMMANDS), + (tacticCategories.HOLE_COMMAND, generalPages.HOLE_COMMANDS), + (tacticCategories.ATTRIBUTE, generalPages.ATTRIBUTES) ] for (category, filename) in types_of_tactics: - entries = [e for e in tactic_docs if e[tactic['CATEGORY']] == category] + entries = [e for e in tactic_docs if e[tactic.CATEGORY] == category] with open_outfile(filename + '.html') as out: out.write(env.get_template(filename + '.j2').render( active_path='', - entries = sorted(entries, key = lambda n: n[tactic['NAME']]), - tagset = sorted(set(t for e in entries for t in e[tactic['TAGS']])) + entries = sorted(entries, key = lambda n: n[tactic.NAME]), + tagset = sorted(set(t for e in entries for t in e[tactic.TAGS])) )) for filename, decls in file_map.items(): @@ -398,8 +398,8 @@ def write_html_files(file_map, notes, mod_docs, tactic_docs): out.write(env.get_template('module.j2').render( active_path = filename.url, filename = filename, - items = sorted(md + decls, key = lambda d: d[declaration['LINE']]), - decl_names = sorted(d[declaration['NAME']] for d in decls), + items = sorted(md + decls, key = lambda d: d[declaration.LINE]), + decl_names = sorted(d[declaration.NAME] for d in decls), )) for (filename, displayname, source, _) in EXTRA_DOC_FILES: @@ -409,17 +409,18 @@ def write_site_map(file_map): with open_outfile('sitemap.txt') as out: for filename in file_map: out.write(SITE_ROOT + filename.url + '\n') - for name in generalPages.values(): - out.write(SITE_ROOT + name + '.html\n') + for name in dir(generalPages): + if not name.startswith('__'): + out.write(SITE_ROOT + name + '.html\n') for (filename, _, _, _) in EXTRA_DOC_FILES: out.write(SITE_ROOT + filename + '.html\n') def name_in_decl(decl_name, decl): - if decl[declaration['NAME']] == decl_name: + if decl[declaration.NAME] == decl_name: return True - if decl_name in [sf[0] for sf in decl[declaration['STRUCTURE_FIELDS']]]: + if decl_name in [sf[0] for sf in decl[declaration.STRUCTURE_FIELDS]]: return True - if decl_name in [cnstr[0] for cnstr in decl[declaration['CONSTRUCTORS']]]: + if decl_name in [cnstr[0] for cnstr in decl[declaration.CONSTRUCTORS]]: return True return False @@ -432,7 +433,7 @@ def library_link_from_decl_name(decl_name, decl_loc, file_map): print(f'{decl_name} appears in {decl_loc}, but we do not have data for that declaration. file_map:') print(file_map[decl_loc]) raise e - return library_link(decl_loc, e[declaration['LINE']]) + return library_link(decl_loc, e[declaration.LINE]) def write_docs_redirect(decl_name, decl_loc): url = SITE_ROOT + decl_loc.url @@ -502,13 +503,13 @@ def mk_export_db(file_map): for decls in file_map.values(): for obj in decls: name, filename, kind, is_meta, line, constructors, structure_fields = itemgetter( - declaration['NAME'], - declaration['FILENAME'], - declaration['KIND'], - declaration['IS_META'], - declaration['LINE'], - declaration['CONSTRUCTORS'], - declaration['STRUCTURE_FIELDS'] + declaration.NAME, + declaration.FILENAME, + declaration.KIND, + declaration.IS_META, + declaration.LINE, + declaration.CONSTRUCTORS, + declaration.STRUCTURE_FIELDS )(obj) export_db[name] = mk_export_map_entry(name, filename, kind, is_meta, line) export_db[name]['decl_header_html'] = env.get_template('decl_header.j2').render(decl=obj) @@ -527,11 +528,9 @@ def write_export_db(export_db): def main(): file_map, loc_map, notes, mod_docs, instances, tactic_docs = read_src_data() - setup_jinja_env(file_map, loc_map, instances) - write_decl_txt(loc_map) write_html_files(file_map, notes, mod_docs, tactic_docs) - + write_decl_txt(loc_map) write_redirects(loc_map, file_map) copy_files(MATHLIB_DEST_ROOT, use_symlinks=CLI_ARGS.l) write_export_db(mk_export_db(file_map)) From 15eb701e404cb0333228b63f641f8799605319a4 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Sun, 28 Mar 2021 12:29:15 +0300 Subject: [PATCH 10/25] cleanup comments --- searchWorker.js | 1 - 1 file changed, 1 deletion(-) diff --git a/searchWorker.js b/searchWorker.js index c6a7964..6fadb54 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -1,4 +1,3 @@ -// todo why such a fetch since file is already present here? const req = new XMLHttpRequest(); req.open('GET', 'decl.bmp', false /* blocking */); req.responseType = 'text'; From a37d600756f7a17dd958c75e8ace5212c6beb27b Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Mon, 29 Mar 2021 10:11:29 +0300 Subject: [PATCH 11/25] searchable data export structure --- leanpkg.toml | 4 ++-- print_docs.py | 33 ++++++++++++++++++++++++++++++--- 2 files changed, 32 insertions(+), 5 deletions(-) diff --git a/leanpkg.toml b/leanpkg.toml index d38824a..be99b0b 100644 --- a/leanpkg.toml +++ b/leanpkg.toml @@ -1,8 +1,8 @@ [package] name = "." version = "0.1" -lean_version = "leanprover-community/lean:3.27.0" +lean_version = "leanprover-community/lean:3.28.0" path = "src" [dependencies] -mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "97d13d7561ef9c9a21587cf62324f8b2d215a7f8"} +mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "0e4760b35bdfdfde126f7761f21009637ff08a33"} diff --git a/print_docs.py b/print_docs.py index 47e76fc..678e870 100644 --- a/print_docs.py +++ b/print_docs.py @@ -713,9 +713,9 @@ def mk_export_map_entry(decl_name, filename, kind, is_meta, line, args, tp): 'src_link': library_link(filename, line), 'docs_link': f'{site_root}{filename.url}#{decl_name}'} -def mk_export_db(loc_map, file_map): +def mk_export_db(file_map): export_db = {} - for fn, decls in file_map.items(): + for _, decls in file_map.items(): for obj in decls: export_db[obj['name']] = mk_export_map_entry(obj['name'], obj['filename'], obj['kind'], obj['is_meta'], obj['line'], obj['args'], obj['type']) export_db[obj['name']]['decl_header_html'] = env.get_template('decl_header.j2').render(decl=obj) @@ -730,6 +730,32 @@ def write_export_db(export_db): with gzip.GzipFile(html_root + 'export_db.json.gz', 'w') as zout: zout.write(json_str.encode('utf-8')) +def mk_export_searchable_map_entry(decl_name, filename, descr, kind, args): + return { + 'filename': str(filename.raw_path), + 'name': decl_name, + 'description': descr, + 'kind': kind, + 'args': args, + 'docs_link': f'{site_root}{filename.url}#{decl_name}' + } + +def mk_export_searchable_db(file_map, tactic_docs): + export_searchable_db = {} + for _, decls in file_map.items(): + for obj in decls: + export_searchable_db[obj['name']] = mk_export_map_entry(obj['name'], obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + for (cstr_name, tp) in obj['constructors']: + export_searchable_db[cstr_name] = mk_export_map_entry(cstr_name, obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + for (sf_name, tp) in obj['structure_fields']: + export_searchable_db[sf_name] = mk_export_map_entry(sf_name, obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + return export_searchable_db + +def write_export_searchable_db(searchable_data): + json_str = json.dumps(searchable_data) + with gzip.GzipFile(html_root + 'searchable_data.json.gz', 'w') as zout: + zout.write(json_str.encode('utf-8')) + def main(): bib = parse_bib_file(f'{local_lean_root}docs/references.bib') file_map, loc_map, notes, mod_docs, instances, tactic_docs = load_json() @@ -740,7 +766,8 @@ def main(): copy_css_and_js(html_root, use_symlinks=cl_args.l) copy_yaml_bib_files(html_root) copy_static_files(html_root) - write_export_db(mk_export_db(loc_map, file_map)) + write_export_db(mk_export_db(file_map)) + write_export_searchable_db(mk_export_searchable_db(file_map, tactic_docs)) write_site_map(file_map) if __name__ == '__main__': From ccb7abf4fc79e85c064836adf774b885d744454b Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Mon, 29 Mar 2021 10:23:14 +0300 Subject: [PATCH 12/25] searchable data lists per file name --- print_docs.py | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/print_docs.py b/print_docs.py index 678e870..27fbf8b 100644 --- a/print_docs.py +++ b/print_docs.py @@ -742,13 +742,18 @@ def mk_export_searchable_map_entry(decl_name, filename, descr, kind, args): def mk_export_searchable_db(file_map, tactic_docs): export_searchable_db = {} - for _, decls in file_map.items(): + for fn, decls in file_map.items(): + filename_path = str(fn.raw_path) + export_searchable_db[filename_path] = [] for obj in decls: - export_searchable_db[obj['name']] = mk_export_map_entry(obj['name'], obj['filename'], obj['doc_string'], obj['kind'], obj['args']) - for (cstr_name, tp) in obj['constructors']: - export_searchable_db[cstr_name] = mk_export_map_entry(cstr_name, obj['filename'], obj['doc_string'], obj['kind'], obj['args']) - for (sf_name, tp) in obj['structure_fields']: - export_searchable_db[sf_name] = mk_export_map_entry(sf_name, obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + decl_entry = mk_export_map_entry(obj['name'], obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + export_searchable_db[filename_path].append(decl_entry) + for (cstr_name, _) in obj['constructors']: + cstr_entry = mk_export_map_entry(cstr_name, obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + export_searchable_db[filename_path].append(cstr_entry) + for (sf_name, _) in obj['structure_fields']: + sf_entry = mk_export_map_entry(sf_name, obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + export_searchable_db[filename_path].append(sf_entry) return export_searchable_db def write_export_searchable_db(searchable_data): From e7f6812d1c47e5314274542aab4078ef78ae5ef3 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Sun, 4 Apr 2021 01:55:10 +0300 Subject: [PATCH 13/25] data structure for searching done --- leanpkg.toml | 2 +- print_docs.py | 29 +++++++++++++++++------------ 2 files changed, 18 insertions(+), 13 deletions(-) diff --git a/leanpkg.toml b/leanpkg.toml index be99b0b..2803ec5 100644 --- a/leanpkg.toml +++ b/leanpkg.toml @@ -5,4 +5,4 @@ lean_version = "leanprover-community/lean:3.28.0" path = "src" [dependencies] -mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "0e4760b35bdfdfde126f7761f21009637ff08a33"} +mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "a5b7de0a178fc31eb6a12b2e62c68a0ea8e63a89"} diff --git a/print_docs.py b/print_docs.py index 27fbf8b..7394d4f 100644 --- a/print_docs.py +++ b/print_docs.py @@ -730,36 +730,41 @@ def write_export_db(export_db): with gzip.GzipFile(html_root + 'export_db.json.gz', 'w') as zout: zout.write(json_str.encode('utf-8')) -def mk_export_searchable_map_entry(decl_name, filename, descr, kind, args): +def mk_export_searchable_map_entry(name, description, kind = '', attributes = []): return { - 'filename': str(filename.raw_path), - 'name': decl_name, - 'description': descr, + 'name': name, + 'description': description, 'kind': kind, - 'args': args, - 'docs_link': f'{site_root}{filename.url}#{decl_name}' + 'attributes': attributes, } def mk_export_searchable_db(file_map, tactic_docs): export_searchable_db = {} + for fn, decls in file_map.items(): - filename_path = str(fn.raw_path) + filename_path = str(fn.url) export_searchable_db[filename_path] = [] for obj in decls: - decl_entry = mk_export_map_entry(obj['name'], obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + decl_entry = mk_export_searchable_map_entry(obj['name'], obj['doc_string'], obj['kind'], obj['attributes']) export_searchable_db[filename_path].append(decl_entry) for (cstr_name, _) in obj['constructors']: - cstr_entry = mk_export_map_entry(cstr_name, obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + cstr_entry = mk_export_searchable_map_entry(cstr_name, obj['doc_string'], obj['kind'], obj['attributes']) export_searchable_db[filename_path].append(cstr_entry) for (sf_name, _) in obj['structure_fields']: - sf_entry = mk_export_map_entry(sf_name, obj['filename'], obj['doc_string'], obj['kind'], obj['args']) + sf_entry = mk_export_searchable_map_entry(sf_name, obj['doc_string'], obj['kind'], obj['attributes']) export_searchable_db[filename_path].append(sf_entry) + + export_searchable_db['tactics.html'] = [] + for tactic in tactic_docs: + tactic_entry = mk_export_searchable_map_entry(tactic['name'], tactic['description']) + export_searchable_db['tactics.html'].append(tactic_entry) + return export_searchable_db def write_export_searchable_db(searchable_data): json_str = json.dumps(searchable_data) - with gzip.GzipFile(html_root + 'searchable_data.json.gz', 'w') as zout: - zout.write(json_str.encode('utf-8')) + with open_outfile('searchable_data.json') as out: + out.write(json_str) def main(): bib = parse_bib_file(f'{local_lean_root}docs/references.bib') From d8212ca521e1b8ed9e3e3ccd545fe4bf5aba1b7f Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Sat, 1 May 2021 14:08:08 +0300 Subject: [PATCH 14/25] searchable json holds files togethere with declarations --- print_docs.py | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/print_docs.py b/print_docs.py index 7394d4f..e51695c 100644 --- a/print_docs.py +++ b/print_docs.py @@ -730,8 +730,9 @@ def write_export_db(export_db): with gzip.GzipFile(html_root + 'export_db.json.gz', 'w') as zout: zout.write(json_str.encode('utf-8')) -def mk_export_searchable_map_entry(name, description, kind = '', attributes = []): +def mk_export_searchable_map_entry(filename_name, name, description, kind = '', attributes = []): return { + 'module': filename_name, 'name': name, 'description': description, 'kind': kind, @@ -739,25 +740,26 @@ def mk_export_searchable_map_entry(name, description, kind = '', attributes = [] } def mk_export_searchable_db(file_map, tactic_docs): - export_searchable_db = {} + export_searchable_db = [] for fn, decls in file_map.items(): - filename_path = str(fn.url) - export_searchable_db[filename_path] = [] + filename_name = str(fn.url) for obj in decls: - decl_entry = mk_export_searchable_map_entry(obj['name'], obj['doc_string'], obj['kind'], obj['attributes']) - export_searchable_db[filename_path].append(decl_entry) + decl_entry = mk_export_searchable_map_entry(filename_name, obj['name'], obj['doc_string'], obj['kind'], obj['attributes']) + export_searchable_db.append(decl_entry) for (cstr_name, _) in obj['constructors']: - cstr_entry = mk_export_searchable_map_entry(cstr_name, obj['doc_string'], obj['kind'], obj['attributes']) - export_searchable_db[filename_path].append(cstr_entry) + cstr_entry = mk_export_searchable_map_entry(filename_name, cstr_name, obj['doc_string'], obj['kind'], obj['attributes']) + export_searchable_db.append(cstr_entry) for (sf_name, _) in obj['structure_fields']: - sf_entry = mk_export_searchable_map_entry(sf_name, obj['doc_string'], obj['kind'], obj['attributes']) - export_searchable_db[filename_path].append(sf_entry) + sf_entry = mk_export_searchable_map_entry(filename_name, sf_name, obj['doc_string'], obj['kind'], obj['attributes']) + export_searchable_db.append(sf_entry) - export_searchable_db['tactics.html'] = [] for tactic in tactic_docs: - tactic_entry = mk_export_searchable_map_entry(tactic['name'], tactic['description']) - export_searchable_db['tactics.html'].append(tactic_entry) + # category is the singular form of each docs webpage in 'General documentation' + # e.g. 'tactic' -> 'tactics.html' + tactic_entry_container_name = f"{tactic['category']}s.html" + tactic_entry = mk_export_searchable_map_entry(tactic_entry_container_name, tactic['name'], tactic['description']) + export_searchable_db.append(tactic_entry) return export_searchable_db From 8d4da8858a98b3cc82a10688458781519e3d9db6 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Mon, 3 May 2021 16:28:30 +0300 Subject: [PATCH 15/25] building leanpkg increases commit # --- leanpkg.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/leanpkg.toml b/leanpkg.toml index 2803ec5..d2a7cbd 100644 --- a/leanpkg.toml +++ b/leanpkg.toml @@ -5,4 +5,4 @@ lean_version = "leanprover-community/lean:3.28.0" path = "src" [dependencies] -mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "a5b7de0a178fc31eb6a12b2e62c68a0ea8e63a89"} +mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "62c06a557ad0a3496d31c9462e60763b9e7bf4ec"} From 8dddd0a344491515fe518a92fc222e6a8f5c2c72 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Wed, 5 May 2021 00:25:05 +0300 Subject: [PATCH 16/25] searching through index; styling; WIP filters --- nav.js | 156 ++++++++++++++++++++++++++++++---------------- searchWorker.js | 77 +++++++++++++++++------ style.css | 128 +++++++++++++++++++------------------ templates/base.j2 | 7 ++- 4 files changed, 232 insertions(+), 136 deletions(-) diff --git a/nav.js b/nav.js index c8a522a..5d2ed10 100644 --- a/nav.js +++ b/nav.js @@ -91,44 +91,35 @@ if (tse !== null) { }); } -// Simple search through declarations by name +// Simple search through declarations by name, file name and description comment as printed from mathlib directly // ------------------------- -const searchWorkerURL = new URL(`${siteRoot}searchWorker.js`, window.location); -const declSearch = (query) => new Promise((resolve, reject) => { - const worker = new SharedWorker(searchWorkerURL); - worker.port.start(); - worker.port.onmessage = ({ data }) => resolve(data); - worker.port.onmessageerror = (e) => reject(e); - worker.port.postMessage({ query }); -}); - -const resultsElmntId = 'search_results'; -document.getElementById('search_form') - .appendChild(document.createElement('div')) - .id = resultsElmntId; // todo add on creation of page, not here +const searchForm = document.getElementById('search_form'); +const searchQuery = searchForm.querySelector('input[name=query]'); +const searchResults = document.getElementById('search_results'); +const maxCountResults = 150; -function handleSearchCursorUpDown(down) { - const selectedResult = document.querySelector(`#${resultsElmntId} .selected`); - const resultsElmnt = document.getElementById(resultsElmntId); - - let toSelect = down ? resultsElmnt.firstChild : resultsElmnt.lastChild; - if (selectedResult) { - selectedResult.classList.remove('selected'); - toSelect = down ? selectedResult.nextSibling : selectedResult.previousSibling; +searchQuery.addEventListener('keydown', (ev) => { + if (!searchQuery.value || searchQuery.value.length === 0) { + searchResults.innerHTML = ''; + } else { + switch (ev.key) { + case 'Down': + case 'ArrowDown': + ev.preventDefault(); + handleSearchCursorUpDown(true); + break; + case 'Up': + case 'ArrowUp': + ev.preventDefault(); + handleSearchCursorUpDown(false); + break; + } } - toSelect && toSelect.classList.add('selected'); -} - -function handleSearchItemSelected() { - const selectedResult = document.querySelector(`#${resultsElmntId} .selected`) - selectedResult.click(); -} - -const searchInputElmnt = document.querySelector('#search_form input[name=q]'); + +}); -// todo use Enter to start searching if we still in and not
    -searchInputElmnt.addEventListener('keydown', (ev) => { +searchResults.addEventListener('keydown', (ev) => { switch (ev.key) { case 'Down': case 'ArrowDown': @@ -147,36 +138,91 @@ searchInputElmnt.addEventListener('keydown', (ev) => { } }); -searchInputElmnt.addEventListener('input', async (ev) => { - const text = ev.target.value; +function handleSearchCursorUpDown(isDownwards) { + const selectedResult = document.querySelector(`#${resultsElmntId} .selected`); - if (!text) { - const resultsElmnt = document.getElementById(resultsElmntId); - resultsElmnt.removeAttribute('state'); - resultsElmnt.replaceWith(resultsElmnt.cloneNode(false)); - return; + if (selectedResult) { + selectedResult.classList.remove('selected'); + selectedResult = isDownwards ? selectedResult.nextSibling : selectedResult.previousSibling; + } else { + selectedResult = isDownwards ? resultsContainer.firstChild : resultsContainer.lastChild; } - document.getElementById(resultsElmntId).setAttribute('state', 'loading'); + selectedResult && selectedResult.classList.add('selected'); +} + +function handleSearchItemSelected() { + // todo goto link made up of the siteRood+module+name + const selectedResult = document.querySelector(`#${resultsElmntId} .selected`) + selectedResult.click(); +} - const result = await declSearch(text); - if (ev.target.value != text) return; // todo why? +// Searching through the index with a specific query and filters +const searchWorkerURL = new URL(`${siteRoot}searchWorker.js`, window.location); +const worker = new SharedWorker(searchWorkerURL); +const searchIndexedData = (query) => new Promise((resolve, reject) => { + // todo remove when UI filters done + const filters = { + attributes: ['nolint'], + // kind: ['def'] + }; - const currentResultsElmnt = document.getElementById('search_results'); - const resultsElmntCopy = currentResultsElmnt.cloneNode(false); - for (const { decl } of result) { - const d = resultsElmntCopy.appendChild(document.createElement('a')); - d.innerText = decl; - d.title = decl; - d.href = `${siteRoot}find/${decl}`; - } - resultsElmntCopy.setAttribute('state', 'done'); - currentResultsElmnt.replaceWith(resultsElmntCopy); + worker.port.start(); + worker.port.onmessage = ({ data }) => resolve(data); + worker.port.onmessageerror = (e) => reject(e); + worker.port.postMessage({ query, maxCount: maxCountResults, filters }); }); +const submitSearchFormHandler = async (ev) => { + ev.preventDefault(); + const query = searchQuery.value; + + if (!query && query.length <= 0) { + // todo not needed? + return; + } + + searchResults.setAttribute('state', 'loading'); + await fillInSearchResultsContainer(query); + searchResults.setAttribute('state', 'done'); +}; +searchForm.addEventListener('submit', submitSearchFormHandler); + +const fillInSearchResultsContainer = async (query) => { + const results = await searchIndexedData(query); + results.sort((a, b) => (a && typeof a.score === "number" && b && typeof b.score === "number") ? (b.score - a.score) : 0); + searchResults.innerHTML = results.length < 1 ? createNoResultsHTML() : createResultsHTML(results); +} + +const createNoResultsHTML = () => '

    No declarations or comments match your search.

    '; + +const createResultsHTML = (results) => { + let html = `

    Found ${results.length} matches, showing ${maxCountResults > results.length ? results.length : maxCountResults}.

    `; + html += results.map((result, index) => { + return createSingleResultHTML(result, index); + }).join(''); + return html; +} + +const createSingleResultHTML = (result, i) => { + const { module, name, description, match, terms } = result; + const resultUrl = `${siteRoot}${module}#${name}`; + const descriptionDisplay = description && description.length > 0 ? `${description.slice(0, 150)}..` : '' + + const html = ``; + + return html; +} + // 404 page goodies // ---------------- - const suggestionsElmnt = document.getElementById('howabout'); if (suggestionsElmnt) { suggestionsElmnt.innerText = "Please wait a second. I'll try to help you."; @@ -187,7 +233,7 @@ if (suggestionsElmnt) { .innerText = window.location.href.replace(/[/]/g, '/\u200b'); const query = window.location.href.match(/[/]([^/]+)(?:\.html|[/])?$/)[1]; - declSearch(query).then((results) => { + searchIndexedData(query).then((results) => { suggestionsElmnt.innerText = 'How about one of these instead:'; const ul = suggestionsElmnt.appendChild(document.createElement('ul')); for (const { decl } of results) { diff --git a/searchWorker.js b/searchWorker.js index 6fadb54..9272981 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -1,27 +1,66 @@ +// Access indexed data structure to be used for searching through the documentation const req = new XMLHttpRequest(); -req.open('GET', 'decl.bmp', false /* blocking */); -req.responseType = 'text'; -req.send(); - -const declNames = req.responseText.split('\n'); -// Adapted from the default tokenizer and -// https://util.unicode.org/UnicodeJsps/list-unicodeset.jsp?a=%5Cp%7BZ%7D&abb=on&c=on&esc=on&g=&i= -const SEPARATOR = /[._\n\r \u00A0\u1680\u2000-\u200A\u2028\u2029\u202F\u205F\u3000]+/u +req.open('GET', 'searchable_data.json', false /* blocking */); +req.responseType = 'json'; +req.send(); importScripts('https://cdn.jsdelivr.net/npm/minisearch@2.4.1/dist/umd/index.min.js'); + // Include options as per API specs: https://lucaong.github.io/minisearch/modules/_minisearch_.html const miniSearch = new MiniSearch({ - fields: ['decl'], - storeFields: ['decl'], - tokenize: text => text.split(SEPARATOR), + idField: 'name', + fields: ['module', 'name', 'description'], + storeFields: ['module', 'name', 'description', 'attributes', 'kind'] }); -miniSearch.addAll(declNames.map((decl, id) => ({decl, id}))); + +const indexedData = req.response; +miniSearch.addAll(indexedData); onconnect = ({ports: [port]}) => - port.onmessage = ({data}) => { - const results = miniSearch.search(data.q, { - prefix: (term) => term.length > 3, - fuzzy: (term) => term.length > 3 && 0.2, - }); - port.postMessage(results.slice(0, 20)); - }; +port.onmessage = ({ data }) => { + const { query, filters, maxCount } = data; + const results = miniSearch.search(query, { + boost: { module: 1, description: 2, name: 3 }, + combineWith: 'AND', + filter: (result) => filterItemResult(result, filters), + // prefix: (term) => term.length > 3, + // fuzzy: (term) => term.length > 3 && 0.2, + }); + + console.log(results); + const response = typeof maxCount === "number" ? results.slice(0, maxCount) : results; + port.postMessage(response); +}; + +const filterItemResult = (result, filters = {}) => { + const { attributes: attrFilter, kind: kindFilter } = filters; + const hasAttrFilter = attrFilter && attrFilter.length > 0; + const hasKindFilter = kindFilter && kindFilter.length > 0; + + if (!hasAttrFilter && !hasKindFilter) { + return true; + } + + const { attributes: attrRes, kind: kindRes } = result; + let isResultAttrIncluded = false; + let isResultKindIncluded = false; + + if (hasKindFilter) { + isResultKindIncluded = kindFilter.includes(kindRes); + } + + if (hasAttrFilter) { + for (let attribute of attrRes) { + if (attrFilter.includes(attribute)) { + isResultAttrIncluded = true; + break; + } + } + } + + return hasKindFilter && hasAttrFilter ? + (isResultAttrIncluded && isResultKindIncluded) : + hasAttrFilter ? + isResultAttrIncluded : + isResultKindIncluded; +} \ No newline at end of file diff --git a/style.css b/style.css index 78efc65..212b7cb 100644 --- a/style.css +++ b/style.css @@ -114,8 +114,7 @@ header { @media screen and (max-width: 700px) { header h1 span { display: none; } :root { --header-side-padding: 1ex; } - #search_form button { display: none; } - #search_form input { width: 100%; } + #search_form input { width: 60%; } header #search_results { left: 1ex; right: 1ex; @@ -145,63 +144,6 @@ header header_filename { } } -/* inserted by nav.js */ -#search_results { - position: absolute; - top: var(--header-height); - right: calc(var(--header-side-padding)); - width: calc(20em + 4em); - z-index: 1; - background: var(--header-bg); - border: 1px solid #aaa; - border-top: none; - overflow-x: hidden; - overflow-y: auto; - max-height: calc(100vh - var(--header-height)); -} - -#search_results:empty { - display: none; -} - -#search_results[state="loading"]:empty { - display: block; - cursor: progress; -} -#search_results[state="loading"]:empty::before { - display: block; - content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; - padding: 1ex; - animation: marquee 10s linear infinite; -} -@keyframes marquee { - 0% { transform: translate(100%, 0); } - 100% { transform: translate(-100%, 0); } -} - -#search_results[state="done"]:empty { - display: block; - text-align: center; - padding: 1ex; -} -#search_results[state="done"]:empty::before { - content: '(no results)'; - font-style: italic; -} - -#search_results a { - display: block; - color: inherit; - padding: 1ex; - border-left: 0.5ex solid transparent; - padding-left: 0.5ex; - cursor: pointer; -} -#search_results .selected { - background: white; - border-color: #f0a202; -} - main, nav { margin-top: calc(var(--header-height) + 1em); } @@ -560,3 +502,71 @@ a:hover { margin-top: 2em; margin-bottom: 2em; } + + + +/* Search interface in form for search */ +#search_results { + position: absolute; + top: var(--header-height); + right: calc(var(--header-side-padding)); + width: 35em; + z-index: 1; + background: var(--header-bg); + border: 1px solid #aaa; + border-top: none; + overflow-x: auto; + overflow-y: auto; + max-height: calc(95vh - var(--header-height)); +} + +#search_results:empty { + display: none; +} + +#search_results[state="loading"]:empty { + display: block; + cursor: progress; +} +#search_results[state="loading"]:empty::before { + display: block; + content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; + padding: 1ex; + animation: marquee 10s linear infinite; +} +@keyframes marquee { + 0% { transform: translate(100%, 0); } + 100% { transform: translate(-100%, 0); } +} + +#search_results[state="done"]:empty { + display: block; + text-align: center; + padding: 1ex; +} +#search_results[state="done"]:empty::before { + content: '(no results)'; + font-style: italic; +} + +#search_results a { + display: block; + color: inherit; + padding: 4px; + border-top: 1px dashed #70a0d0; + cursor: pointer; +} +#search_results a .result_module { + font-size: 0.7em; + margin-top: 1px; +} +#search_results a .result_comment { + font-size: 0.8em; + margin-top: -0.5em; + font-family: 'Open Sans', sans-serif; +} + +#search_results .selected { + background: white; + border-color: #f0a202; +} \ No newline at end of file diff --git a/templates/base.j2 b/templates/base.j2 index 129c625..f68be9d 100644 --- a/templates/base.j2 +++ b/templates/base.j2 @@ -28,10 +28,11 @@

    mathlib documentation

    {% block doctitle %}{{ self.title() }}{% endblock %}

    -
    + - - + + +
    From 5432001b36efef84e5f03337ef456f644c5b7caf Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Sat, 8 May 2021 18:03:24 +0300 Subject: [PATCH 17/25] add filters to UI --- nav.js | 162 +++++++++++++++++++++++++++++----------------- searchWorker.js | 2 +- style.css | 43 ++++++++++-- templates/base.j2 | 85 ++++++++++++++++++++++++ 4 files changed, 225 insertions(+), 67 deletions(-) diff --git a/nav.js b/nav.js index 5d2ed10..56ddc07 100644 --- a/nav.js +++ b/nav.js @@ -91,17 +91,81 @@ if (tse !== null) { }); } -// Simple search through declarations by name, file name and description comment as printed from mathlib directly +// Simple search through declarations by name, file name and description comment as printed from mathlib // ------------------------- +const MAX_COUNT_RESULTS = 15; +/* Get all elements for searching and showing results */ const searchForm = document.getElementById('search_form'); -const searchQuery = searchForm.querySelector('input[name=query]'); -const searchResults = document.getElementById('search_results'); -const maxCountResults = 150; +const searchQueryInput = searchForm.querySelector('input[name=query]'); +const searchResultsContainer = document.getElementById('search_results'); -searchQuery.addEventListener('keydown', (ev) => { - if (!searchQuery.value || searchQuery.value.length === 0) { - searchResults.innerHTML = ''; +/* Set up defaults for search filtering and results */ +const filters = {}; +const maxCount = MAX_COUNT_RESULTS; + +/* Handle searching through the index with a specific query and filters */ +const searchWorkerURL = new URL(`${siteRoot}searchWorker.js`, window.location); +const worker = new SharedWorker(searchWorkerURL); +const searchIndexedData = (query) => new Promise((resolve, reject) => { + worker.port.start(); + worker.port.onmessage = ({ data }) => resolve(data); + worker.port.onmessageerror = (e) => reject(e); + worker.port.postMessage({ query, maxCount, filters }); +}); + +/* Submitting search query */ +const submitSearchFormHandler = async (ev) => { + ev.preventDefault(); + const query = searchQueryInput.value; + + if (!query && query.length <= 0) { + return; + } + + searchResultsContainer.setAttribute('state', 'loading'); + await fillInSearchResultsContainer(query); + searchResultsContainer.setAttribute('state', 'done'); +}; +searchForm.addEventListener('submit', submitSearchFormHandler); + +const fillInSearchResultsContainer = async (query) => { + const results = await searchIndexedData(query); + results.sort((a, b) => (a && typeof a.score === "number" && b && typeof b.score === "number") ? (b.score - a.score) : 0); + searchResultsContainer.innerHTML = results.length < 1 ? createNoResultsHTML() : createResultsHTML(results); +} + +const createNoResultsHTML = () => '

    No declarations or comments match your search.

    '; + +const createResultsHTML = (results) => { + let html = `

    Found ${results.length} matches, showing ${maxCountResults > results.length ? results.length : maxCountResults}.

    `; + html += results.map((result, index) => { + return createSingleResultHTML(result, index); + }).join(''); + return html; +} + +const createSingleResultHTML = (result, i) => { + const { module, name, description, match, terms } = result; + const resultUrl = `${siteRoot}${module}#${name}`; + const descriptionDisplay = description && description.length > 0 ? `${description.slice(0, 150)}..` : '' + + const html = ``; + + return html; +} + +/* Keyboard navigation through search input and results */ +searchQueryInput.addEventListener('keydown', (ev) => { + if (!searchQueryInput.value || searchQueryInput.value.length === 0) { + searchResultsContainer.innerHTML = ''; } else { switch (ev.key) { case 'Down': @@ -119,7 +183,7 @@ searchQuery.addEventListener('keydown', (ev) => { }); -searchResults.addEventListener('keydown', (ev) => { +searchResultsContainer.addEventListener('keydown', (ev) => { switch (ev.key) { case 'Down': case 'ArrowDown': @@ -152,74 +216,50 @@ function handleSearchCursorUpDown(isDownwards) { } function handleSearchItemSelected() { - // todo goto link made up of the siteRood+module+name + // todo goto link made up of the siteRoot+module+name const selectedResult = document.querySelector(`#${resultsElmntId} .selected`) selectedResult.click(); } -// Searching through the index with a specific query and filters -const searchWorkerURL = new URL(`${siteRoot}searchWorker.js`, window.location); -const worker = new SharedWorker(searchWorkerURL); -const searchIndexedData = (query) => new Promise((resolve, reject) => { - // todo remove when UI filters done - const filters = { - attributes: ['nolint'], - // kind: ['def'] - }; - worker.port.start(); - worker.port.onmessage = ({ data }) => resolve(data); - worker.port.onmessageerror = (e) => reject(e); - worker.port.postMessage({ query, maxCount: maxCountResults, filters }); -}); -const submitSearchFormHandler = async (ev) => { - ev.preventDefault(); - const query = searchQuery.value; +// Simple filtering by *attributes* and *kind* per declaration +// ------------------------- - if (!query && query.length <= 0) { - // todo not needed? - return; +/* Get all elements for filtering */ +const filtersToggleButton = document.getElementById('search_filtes_btn'); +const filtersContainer = document.getElementById('filters_container'); +const filtersForm = document.getElementById('filters_form'); +const closeFiltersBtn = document.getElementById('close_filters'); + +/* Handle opening/closing filters container */ +filtersToggleButton.addEventListener("click", function() { + const isOpen = filtersContainer.style.display !== 'none'; + + if (isOpen) { + filtersContainer.style.display = 'none'; + } else { + filtersContainer.style.display = 'block'; } +}); - searchResults.setAttribute('state', 'loading'); - await fillInSearchResultsContainer(query); - searchResults.setAttribute('state', 'done'); +/* Handle submit chosen filters */ +const submitFiltersFormHandler = async (ev) => { + ev.preventDefault(); + // todo set filter values to a filter{} and move on + attributesFilters = filtersForm.querySelectorAll('input[name=attributes]:checked').map(e => e.value); + kindFilters = filtersForm.querySelectorAll('input[name=kind]:checked').map(e => e.value); }; -searchForm.addEventListener('submit', submitSearchFormHandler); +filtersForm.addEventListener('submit', submitFiltersFormHandler); -const fillInSearchResultsContainer = async (query) => { - const results = await searchIndexedData(query); - results.sort((a, b) => (a && typeof a.score === "number" && b && typeof b.score === "number") ? (b.score - a.score) : 0); - searchResults.innerHTML = results.length < 1 ? createNoResultsHTML() : createResultsHTML(results); -} +/* Handle closing filters box */ +closeFiltersBtn.addEventListener("click", function() { + filtersContainer.style.display = 'none'; +}); -const createNoResultsHTML = () => '

    No declarations or comments match your search.

    '; -const createResultsHTML = (results) => { - let html = `

    Found ${results.length} matches, showing ${maxCountResults > results.length ? results.length : maxCountResults}.

    `; - html += results.map((result, index) => { - return createSingleResultHTML(result, index); - }).join(''); - return html; -} -const createSingleResultHTML = (result, i) => { - const { module, name, description, match, terms } = result; - const resultUrl = `${siteRoot}${module}#${name}`; - const descriptionDisplay = description && description.length > 0 ? `${description.slice(0, 150)}..` : '' - - const html = ``; - return html; -} // 404 page goodies // ---------------- diff --git a/searchWorker.js b/searchWorker.js index 9272981..f5ee65c 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -28,7 +28,7 @@ port.onmessage = ({ data }) => { }); console.log(results); - const response = typeof maxCount === "number" ? results.slice(0, maxCount) : results; + const response = typeof maxCount === "number" && maxCount >= 0 ? results.slice(0, maxCount) : results; port.postMessage(response); }; diff --git a/style.css b/style.css index 212b7cb..192ab1c 100644 --- a/style.css +++ b/style.css @@ -504,20 +504,53 @@ a:hover { } +/* Form for filtering search through declarations */ +#filters_container { + display: none; + width: 20em; + height: 20em; + position: absolute; + right: calc(var(--header-side-padding)); + top: var(--header-height); + z-index: 0.9; + background: var(--header-bg); + border: 1px solid rgb(218, 216, 216); + border-top: none; + overflow-x: scroll; + overflow-y: hidden; +} -/* Search interface in form for search */ +#filters_container #filters_form { + display: flex; + flex-wrap: wrap; + justify-content: space-around; +} + +/* Style the close button (span) */ +#filters_container #close_filters { + cursor: pointer; + position: absolute; + top: 50%; + right: 0%; + padding: 12px 16px; + transform: translate(0%, -50%); + } + +#filters_container #close_filters:hover {background: #bbb;} + +/* Form for searching through declarations */ #search_results { position: absolute; top: var(--header-height); right: calc(var(--header-side-padding)); - width: 35em; + width: 20em; z-index: 1; background: var(--header-bg); border: 1px solid #aaa; border-top: none; - overflow-x: auto; - overflow-y: auto; - max-height: calc(95vh - var(--header-height)); + overflow-x: scroll; + overflow-y: scroll; + max-height: calc(60vh - var(--header-height)); } #search_results:empty { diff --git a/templates/base.j2 b/templates/base.j2 index f68be9d..07f81f2 100644 --- a/templates/base.j2 +++ b/templates/base.j2 @@ -31,8 +31,93 @@
    +
    +
    + x + +
    + Attributes: +
    + + +
    + + +
    + + +
    + + +
    + + +
    +
    +
    + Kind: +
    + + +
    + + +
    + + +
    + + +
    + + +
    +
    + + +
    From 4c78d9cb2152de6eb829d40d1f89911f01ff37f0 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Wed, 12 May 2021 00:03:44 +0300 Subject: [PATCH 18/25] show all results implementation --- nav.js | 166 ++++++++++++++++++++++++++++++++++++---------- searchWorker.js | 13 +++- style.css | 71 +++++++++++++------- templates/base.j2 | 87 +++++++++++++----------- 4 files changed, 235 insertions(+), 102 deletions(-) diff --git a/nav.js b/nav.js index 56ddc07..358bab5 100644 --- a/nav.js +++ b/nav.js @@ -93,21 +93,58 @@ if (tse !== null) { // Simple search through declarations by name, file name and description comment as printed from mathlib // ------------------------- -const MAX_COUNT_RESULTS = 15; +const MAX_COUNT_RESULTS = 10; /* Get all elements for searching and showing results */ const searchForm = document.getElementById('search_form'); const searchQueryInput = searchForm.querySelector('input[name=query]'); const searchResultsContainer = document.getElementById('search_results'); +/* Handle opening/closing search results container */ +function closeResultsDisplay() { + searchResultsContainer.style.display = 'none'; +} + +function openResultsDisplay() { + searchResultsContainer.style.display = 'block'; +} + +/* Handle resizing search results container */ +function renderSmallResultsContainer() { + searchResultsContainer.classList.contains('full_width') + ? + searchResultsContainer.classList.contains('condensed') + ? + searchResultsContainer.classList.remove('full_width') + : + searchResultsContainer.classList.replace('full_width', 'condensed') + : + !searchResultsContainer.classList.contains('condensed') && searchResultsContainer.classList.add('condensed'); +} + +function renderLargeResultsContainer() { + searchResultsContainer.classList.contains('condensed') + ? + searchResultsContainer.classList.contains('full_width') + ? + searchResultsContainer.classList.remove('condensed') + : + searchResultsContainer.classList.replace('condensed', 'full_width') + : + !searchResultsContainer.classList.contains('full_width') && searchResultsContainer.classList.add('full_width'); +} /* Set up defaults for search filtering and results */ -const filters = {}; -const maxCount = MAX_COUNT_RESULTS; +const filters = { + attributes: [], + kind: [] +}; /* Handle searching through the index with a specific query and filters */ const searchWorkerURL = new URL(`${siteRoot}searchWorker.js`, window.location); const worker = new SharedWorker(searchWorkerURL); -const searchIndexedData = (query) => new Promise((resolve, reject) => { +const searchIndexedData = (query, maxResultsCount) => new Promise((resolve, reject) => { + const maxCount = typeof maxResultsCount === "number" ? maxResultsCount : MAX_COUNT_RESULTS; + worker.port.start(); worker.port.onmessage = ({ data }) => resolve(data); worker.port.onmessageerror = (e) => reject(e); @@ -117,39 +154,83 @@ const searchIndexedData = (query) => new Promise((resolve, reject) => { /* Submitting search query */ const submitSearchFormHandler = async (ev) => { ev.preventDefault(); + closeFiltersDisplay(); + const query = searchQueryInput.value; - if (!query && query.length <= 0) { + closeResultsDisplay(); return; } + renderSmallResultsContainer(); + openResultsDisplay(); + searchResultsContainer.setAttribute('state', 'loading'); await fillInSearchResultsContainer(query); searchResultsContainer.setAttribute('state', 'done'); + + const searchResultsContainerCloseBtn = document.getElementById('close_results_btn'); + searchResultsContainerCloseBtn.addEventListener("click", closeResultsDisplay); + + const searchResultsShowAllBtn = document.getElementById('show_all_results_btn'); + searchResultsShowAllBtn.addEventListener('click', () => renderAllResultsHtml(query)); }; searchForm.addEventListener('submit', submitSearchFormHandler); -const fillInSearchResultsContainer = async (query) => { - const results = await searchIndexedData(query); - results.sort((a, b) => (a && typeof a.score === "number" && b && typeof b.score === "number") ? (b.score - a.score) : 0); - searchResultsContainer.innerHTML = results.length < 1 ? createNoResultsHTML() : createResultsHTML(results); +const renderAllResultsHtml = async (query) => { + if (!query && query.length <= 0) { + closeResultsDisplay(); + return; + } + renderLargeResultsContainer(); + openResultsDisplay(); + + + searchResultsContainer.setAttribute('state', 'loading'); + await fillInSearchResultsContainer(query, true); + searchResultsContainer.setAttribute('state', 'done'); + + const searchResultsContainerCloseBtn = document.getElementById('close_results_btn'); + searchResultsContainerCloseBtn.addEventListener("click", closeResultsDisplay); } -const createNoResultsHTML = () => '

    No declarations or comments match your search.

    '; +const fillInSearchResultsContainer = async (query, showAll = false) => { + const resultsCount = showAll ? -1 : MAX_COUNT_RESULTS; + const {response: results, total} = await searchIndexedData(query, resultsCount); + results.sort((a, b) => (a && typeof a.score === "number" && b && typeof b.score === "number") ? (b.score - a.score) : 0); + + const searchResultsCloseBtn = 'x'; + searchResultsContainer.innerHTML = results.length < 1 ? createNoResultsHTML(searchResultsCloseBtn) : createResultsHTML(results, total, showAll, searchResultsCloseBtn); +} -const createResultsHTML = (results) => { - let html = `

    Found ${results.length} matches, showing ${maxCountResults > results.length ? results.length : maxCountResults}.

    `; - html += results.map((result, index) => { - return createSingleResultHTML(result, index); +const createNoResultsHTML = (html) => `

    No declarations or comments match your search.

    ${html}`; + +const createResultsHTML = (results, total, showAll, html) => { + const descriptionMaxLength = showAll ? 350 : 80; + let resultHtml = `

    Found ${total} matches + ${!showAll + ? + `, showing ${MAX_COUNT_RESULTS > results.length ? results.length : MAX_COUNT_RESULTS}.

    + Show all` + : + '' + } + ${html}`; + resultHtml += results.map((result, index) => { + return createSingleResultHTML(result, descriptionMaxLength, index); }).join(''); - return html; + return resultHtml; } -const createSingleResultHTML = (result, i) => { +const createSingleResultHTML = (result, descriptionMaxLength, i) => { const { module, name, description, match, terms } = result; const resultUrl = `${siteRoot}${module}#${name}`; - const descriptionDisplay = description && description.length > 0 ? `${description.slice(0, 150)}..` : '' - + const descriptionDisplay = description && description.length > 0 + ? + `${description.slice(0, descriptionMaxLength)}${description.length > descriptionMaxLength ? '..' : ''}` + : + ''; + const html = `
    ${name} @@ -216,7 +297,6 @@ function handleSearchCursorUpDown(isDownwards) { } function handleSearchItemSelected() { - // todo goto link made up of the siteRoot+module+name const selectedResult = document.querySelector(`#${resultsElmntId} .selected`) selectedResult.click(); } @@ -227,36 +307,50 @@ function handleSearchItemSelected() { // ------------------------- /* Get all elements for filtering */ -const filtersToggleButton = document.getElementById('search_filtes_btn'); +const filtersToggleButton = document.getElementById('search_filters_btn'); const filtersContainer = document.getElementById('filters_container'); const filtersForm = document.getElementById('filters_form'); -const closeFiltersBtn = document.getElementById('close_filters'); +const closeFiltersBtn = document.getElementById('close_filters_btn'); /* Handle opening/closing filters container */ -filtersToggleButton.addEventListener("click", function() { - const isOpen = filtersContainer.style.display !== 'none'; +function closeFiltersDisplay() { + filtersContainer.style.display = 'none'; +} +function openFiltersDisplay() { + filtersContainer.style.display = 'block'; +} + +function toggleFiltersDisplay() { + const filtersContainerStyle = (!filtersContainer.style.display || filtersContainer.style.display.length === 0) ? + getComputedStyle(filtersContainer).display : + filtersContainer.style.display; + const isOpen = filtersContainerStyle !== 'none'; if (isOpen) { - filtersContainer.style.display = 'none'; + closeFiltersDisplay(); } else { - filtersContainer.style.display = 'block'; + openFiltersDisplay(); } -}); +} +filtersToggleButton && filtersToggleButton.addEventListener("click", toggleFiltersDisplay); +filtersContainer && closeFiltersBtn.addEventListener("click", closeFiltersDisplay); /* Handle submit chosen filters */ -const submitFiltersFormHandler = async (ev) => { +const submitFiltersFormHandler = (ev) => { ev.preventDefault(); - // todo set filter values to a filter{} and move on - attributesFilters = filtersForm.querySelectorAll('input[name=attributes]:checked').map(e => e.value); - kindFilters = filtersForm.querySelectorAll('input[name=kind]:checked').map(e => e.value); -}; -filtersForm.addEventListener('submit', submitFiltersFormHandler); + const attributeBoxNodes = filtersForm.querySelectorAll('input[name=attribute]:checked'); + const kindBoxNodes = filtersForm.querySelectorAll('input[name=kind]:checked'); -/* Handle closing filters box */ -closeFiltersBtn.addEventListener("click", function() { - filtersContainer.style.display = 'none'; -}); + + filters.attributes = []; + attributeBoxNodes.forEach(e => filters.attributes.push(e.value)); + filters.kind = []; + kindBoxNodes.forEach(e => filters.kind.push(e.value)); + + closeFiltersDisplay(); +}; +filtersForm && filtersForm.addEventListener('submit', submitFiltersFormHandler); diff --git a/searchWorker.js b/searchWorker.js index f5ee65c..ac515df 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -19,17 +19,18 @@ miniSearch.addAll(indexedData); onconnect = ({ports: [port]}) => port.onmessage = ({ data }) => { const { query, filters, maxCount } = data; + const filterFunc = (result) => filterItemResult(result, filters); const results = miniSearch.search(query, { boost: { module: 1, description: 2, name: 3 }, combineWith: 'AND', - filter: (result) => filterItemResult(result, filters), + filter: filterFunc, // prefix: (term) => term.length > 3, // fuzzy: (term) => term.length > 3 && 0.2, }); console.log(results); const response = typeof maxCount === "number" && maxCount >= 0 ? results.slice(0, maxCount) : results; - port.postMessage(response); + port.postMessage({response, total: results.length}); }; const filterItemResult = (result, filters = {}) => { @@ -38,6 +39,7 @@ const filterItemResult = (result, filters = {}) => { const hasKindFilter = kindFilter && kindFilter.length > 0; if (!hasAttrFilter && !hasKindFilter) { + console.log('NO FILTERS') return true; } @@ -45,14 +47,21 @@ const filterItemResult = (result, filters = {}) => { let isResultAttrIncluded = false; let isResultKindIncluded = false; + console.log('-------------------------------------------') + console.log(`attrRes: ${attrRes}`) + console.log(`attrFilter: ${attrFilter}`) + console.log(`kindRes: ${kindRes}`) + console.log(`kindFilter: ${kindFilter}`) if (hasKindFilter) { isResultKindIncluded = kindFilter.includes(kindRes); + isResultKindIncluded && console.log('kind has passed') } if (hasAttrFilter) { for (let attribute of attrRes) { if (attrFilter.includes(attribute)) { isResultAttrIncluded = true; + console.log('attribute has passed') break; } } diff --git a/style.css b/style.css index 192ab1c..e16cccb 100644 --- a/style.css +++ b/style.css @@ -507,52 +507,73 @@ a:hover { /* Form for filtering search through declarations */ #filters_container { display: none; - width: 20em; - height: 20em; + width: 300px; + height: 250px; position: absolute; right: calc(var(--header-side-padding)); top: var(--header-height); - z-index: 0.9; background: var(--header-bg); border: 1px solid rgb(218, 216, 216); border-top: none; - overflow-x: scroll; - overflow-y: hidden; + overflow-y: auto; + overflow-x: hidden; } -#filters_container #filters_form { +#filters_container #filters_display { display: flex; flex-wrap: wrap; justify-content: space-around; + margin-top: 16px; + margin-bottom: 16px; } /* Style the close button (span) */ -#filters_container #close_filters { +#filters_container #close_filters_btn, +#search_results #close_results_btn { cursor: pointer; position: absolute; - top: 50%; + top: 5px; right: 0%; - padding: 12px 16px; + padding: 0 8px 0 8px; + margin: 8px; transform: translate(0%, -50%); } -#filters_container #close_filters:hover {background: #bbb;} +#filters_container #close_filters_btn:hover {background: #bbb;} +#search_results #close_results_btn:hover {background: #bbb;} +#filters_container #submit_filters_btn { + position: relative; + left: 35%; +} /* Form for searching through declarations */ #search_results { + display: none; position: absolute; top: var(--header-height); right: calc(var(--header-side-padding)); - width: 20em; + width: 380px; z-index: 1; background: var(--header-bg); border: 1px solid #aaa; border-top: none; - overflow-x: scroll; - overflow-y: scroll; + overflow-x: auto; + overflow-y: auto; max-height: calc(60vh - var(--header-height)); } +#search_results.condensed { + width: 380px; + max-height: calc(60vh - var(--header-height)); +} + +#search_results.full_width { + width: 1080px; + max-height: calc(95vh - var(--header-height)); + border: 1px solid #aaa; + box-shadow: 5px 3px 0.8em #60a0b0, -0.5em 0 0.8em #60a0b0; +} + #search_results:empty { display: none; } @@ -563,7 +584,7 @@ a:hover { } #search_results[state="loading"]:empty::before { display: block; - content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; + content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; padding: 1ex; animation: marquee 10s linear infinite; } @@ -572,28 +593,22 @@ a:hover { 100% { transform: translate(-100%, 0); } } -#search_results[state="done"]:empty { - display: block; - text-align: center; - padding: 1ex; -} -#search_results[state="done"]:empty::before { - content: '(no results)'; - font-style: italic; +#search-results #search_info { + font-size: 50%; } -#search_results a { +#search_results .search_result_item a { display: block; color: inherit; padding: 4px; border-top: 1px dashed #70a0d0; cursor: pointer; } -#search_results a .result_module { +#search_results .search_result_item a .result_module { font-size: 0.7em; margin-top: 1px; } -#search_results a .result_comment { +#search_results .search_result_item a .result_comment { font-size: 0.8em; margin-top: -0.5em; font-family: 'Open Sans', sans-serif; @@ -602,4 +617,10 @@ a:hover { #search_results .selected { background: white; border-color: #f0a202; +} + +.link_coloring { + color: hsl(210, 100%, 30%); + text-decoration: none; + cursor: pointer; } \ No newline at end of file diff --git a/templates/base.j2 b/templates/base.j2 index 07f81f2..83d4cc2 100644 --- a/templates/base.j2 +++ b/templates/base.j2 @@ -31,47 +31,49 @@
    - +
    -
    - x - + +
    + x +
    +
    Attributes:





    @@ -80,45 +82,52 @@ Kind:


    - +


    + + +
    - - -
    - +
    + + +
    From 3d52ff224599ae346336e667a10bef1f900015e3 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Wed, 12 May 2021 17:59:47 +0300 Subject: [PATCH 19/25] clean up and version of mathlib commits up --- leanpkg.toml | 4 ++-- searchWorker.js | 9 --------- 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/leanpkg.toml b/leanpkg.toml index d2a7cbd..56936c3 100644 --- a/leanpkg.toml +++ b/leanpkg.toml @@ -1,8 +1,8 @@ [package] name = "." version = "0.1" -lean_version = "leanprover-community/lean:3.28.0" +lean_version = "leanprover-community/lean:3.30.0" path = "src" [dependencies] -mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "62c06a557ad0a3496d31c9462e60763b9e7bf4ec"} +mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "6ee8f0e27f9bf253cd16235367eaecaae86dc5ab"} diff --git a/searchWorker.js b/searchWorker.js index ac515df..eb35701 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -28,7 +28,6 @@ port.onmessage = ({ data }) => { // fuzzy: (term) => term.length > 3 && 0.2, }); - console.log(results); const response = typeof maxCount === "number" && maxCount >= 0 ? results.slice(0, maxCount) : results; port.postMessage({response, total: results.length}); }; @@ -39,7 +38,6 @@ const filterItemResult = (result, filters = {}) => { const hasKindFilter = kindFilter && kindFilter.length > 0; if (!hasAttrFilter && !hasKindFilter) { - console.log('NO FILTERS') return true; } @@ -47,21 +45,14 @@ const filterItemResult = (result, filters = {}) => { let isResultAttrIncluded = false; let isResultKindIncluded = false; - console.log('-------------------------------------------') - console.log(`attrRes: ${attrRes}`) - console.log(`attrFilter: ${attrFilter}`) - console.log(`kindRes: ${kindRes}`) - console.log(`kindFilter: ${kindFilter}`) if (hasKindFilter) { isResultKindIncluded = kindFilter.includes(kindRes); - isResultKindIncluded && console.log('kind has passed') } if (hasAttrFilter) { for (let attribute of attrRes) { if (attrFilter.includes(attribute)) { isResultAttrIncluded = true; - console.log('attribute has passed') break; } } From 0028904d9814f6e296988df1d2483229afd963b7 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Fri, 14 May 2021 18:22:55 +0300 Subject: [PATCH 20/25] filter searching on top of results --- nav.js | 1 + searchWorker.js | 1 + style.css | 3 ++- 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/nav.js b/nav.js index 358bab5..a1d4655 100644 --- a/nav.js +++ b/nav.js @@ -349,6 +349,7 @@ const submitFiltersFormHandler = (ev) => { kindBoxNodes.forEach(e => filters.kind.push(e.value)); closeFiltersDisplay(); + submitSearchFormHandler(ev); }; filtersForm && filtersForm.addEventListener('submit', submitFiltersFormHandler); diff --git a/searchWorker.js b/searchWorker.js index eb35701..0ca91b6 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -29,6 +29,7 @@ port.onmessage = ({ data }) => { }); const response = typeof maxCount === "number" && maxCount >= 0 ? results.slice(0, maxCount) : results; + console.log(response) port.postMessage({response, total: results.length}); }; diff --git a/style.css b/style.css index e16cccb..ebd1806 100644 --- a/style.css +++ b/style.css @@ -517,6 +517,7 @@ a:hover { border-top: none; overflow-y: auto; overflow-x: hidden; + z-index: 2; } #filters_container #filters_display { @@ -584,7 +585,7 @@ a:hover { } #search_results[state="loading"]:empty::before { display: block; - content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; + content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; padding: 1ex; animation: marquee 10s linear infinite; } From c7a94a32ec0f393c08e838a231cca36651d4a1d5 Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Fri, 14 May 2021 18:35:04 +0300 Subject: [PATCH 21/25] lean version reference --- leanpkg.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/leanpkg.toml b/leanpkg.toml index 56936c3..39dc159 100644 --- a/leanpkg.toml +++ b/leanpkg.toml @@ -5,4 +5,4 @@ lean_version = "leanprover-community/lean:3.30.0" path = "src" [dependencies] -mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "6ee8f0e27f9bf253cd16235367eaecaae86dc5ab"} +mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "87adde497c62a4e4e8fdd0fd5cfc46a2d1bd5371"} From ada2c1adb6393709fed939c34af798f348b4c14d Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Sat, 15 May 2021 17:17:00 +0300 Subject: [PATCH 22/25] no errors on nullable elements; add loading when render all too slow --- nav.js | 66 ++++++++++++++++++++++++------------------------- searchWorker.js | 26 ++++++++++--------- 2 files changed, 48 insertions(+), 44 deletions(-) diff --git a/nav.js b/nav.js index a1d4655..895cdc7 100644 --- a/nav.js +++ b/nav.js @@ -110,28 +110,30 @@ function openResultsDisplay() { } /* Handle resizing search results container */ +const SMALL = 'condensed'; +const LARGE = 'full_width'; function renderSmallResultsContainer() { - searchResultsContainer.classList.contains('full_width') + searchResultsContainer.classList.contains(LARGE) ? - searchResultsContainer.classList.contains('condensed') + searchResultsContainer.classList.contains(SMALL) ? - searchResultsContainer.classList.remove('full_width') + searchResultsContainer.classList.remove(LARGE) : - searchResultsContainer.classList.replace('full_width', 'condensed') + searchResultsContainer.classList.replace(LARGE, SMALL) : - !searchResultsContainer.classList.contains('condensed') && searchResultsContainer.classList.add('condensed'); + !searchResultsContainer.classList.contains(SMALL) && searchResultsContainer.classList.add(SMALL); } function renderLargeResultsContainer() { - searchResultsContainer.classList.contains('condensed') + searchResultsContainer.classList.contains(SMALL) ? - searchResultsContainer.classList.contains('full_width') + searchResultsContainer.classList.contains(LARGE) ? - searchResultsContainer.classList.remove('condensed') + searchResultsContainer.classList.remove(SMALL) : - searchResultsContainer.classList.replace('condensed', 'full_width') + searchResultsContainer.classList.replace(SMALL, LARGE) : - !searchResultsContainer.classList.contains('full_width') && searchResultsContainer.classList.add('full_width'); + !searchResultsContainer.classList.contains(LARGE) && searchResultsContainer.classList.add(LARGE); } /* Set up defaults for search filtering and results */ const filters = { @@ -153,11 +155,11 @@ const searchIndexedData = (query, maxResultsCount) => new Promise((resolve, reje /* Submitting search query */ const submitSearchFormHandler = async (ev) => { - ev.preventDefault(); + ev?.preventDefault(); closeFiltersDisplay(); const query = searchQueryInput.value; - if (!query && query.length <= 0) { + if (!query || query.length <= 0) { closeResultsDisplay(); return; } @@ -170,10 +172,10 @@ const submitSearchFormHandler = async (ev) => { searchResultsContainer.setAttribute('state', 'done'); const searchResultsContainerCloseBtn = document.getElementById('close_results_btn'); - searchResultsContainerCloseBtn.addEventListener("click", closeResultsDisplay); + searchResultsContainerCloseBtn?.addEventListener("click", closeResultsDisplay); const searchResultsShowAllBtn = document.getElementById('show_all_results_btn'); - searchResultsShowAllBtn.addEventListener('click', () => renderAllResultsHtml(query)); + searchResultsShowAllBtn?.addEventListener('click', () => renderAllResultsHtml(query)); }; searchForm.addEventListener('submit', submitSearchFormHandler); @@ -182,19 +184,20 @@ const renderAllResultsHtml = async (query) => { closeResultsDisplay(); return; } - renderLargeResultsContainer(); - openResultsDisplay(); - searchResultsContainer.setAttribute('state', 'loading'); await fillInSearchResultsContainer(query, true); + + renderLargeResultsContainer(); + openResultsDisplay(); searchResultsContainer.setAttribute('state', 'done'); const searchResultsContainerCloseBtn = document.getElementById('close_results_btn'); - searchResultsContainerCloseBtn.addEventListener("click", closeResultsDisplay); + searchResultsContainerCloseBtn?.addEventListener("click", closeResultsDisplay); } const fillInSearchResultsContainer = async (query, showAll = false) => { + searchResultsContainer.innerHTML = ''; const resultsCount = showAll ? -1 : MAX_COUNT_RESULTS; const {response: results, total} = await searchIndexedData(query, resultsCount); results.sort((a, b) => (a && typeof a.score === "number" && b && typeof b.score === "number") ? (b.score - a.score) : 0); @@ -207,12 +210,11 @@ const createNoResultsHTML = (html) => `

    No declarati const createResultsHTML = (results, total, showAll, html) => { const descriptionMaxLength = showAll ? 350 : 80; + const countShowingResults = MAX_COUNT_RESULTS > results.length ? results.length : MAX_COUNT_RESULTS; + let resultHtml = `

    Found ${total} matches - ${!showAll - ? - `, showing ${MAX_COUNT_RESULTS > results.length ? results.length : MAX_COUNT_RESULTS}.

    - Show all` - : + ${!showAll ? + `, showing ${countShowingResults}.

    Show all` : '' } ${html}`; @@ -223,12 +225,10 @@ const createResultsHTML = (results, total, showAll, html) => { } const createSingleResultHTML = (result, descriptionMaxLength, i) => { - const { module, name, description, match, terms } = result; + const { module, name, description } = result; const resultUrl = `${siteRoot}${module}#${name}`; - const descriptionDisplay = description && description.length > 0 - ? - `${description.slice(0, descriptionMaxLength)}${description.length > descriptionMaxLength ? '..' : ''}` - : + const descriptionDisplay = description && description.length > 0 ? + `${description.slice(0, descriptionMaxLength)}${description.length > descriptionMaxLength ? '..' : ''}` : ''; const html = `
    @@ -316,6 +316,7 @@ const closeFiltersBtn = document.getElementById('close_filters_btn'); function closeFiltersDisplay() { filtersContainer.style.display = 'none'; } +closeFiltersBtn.addEventListener("click", closeFiltersDisplay); function openFiltersDisplay() { filtersContainer.style.display = 'block'; @@ -332,8 +333,7 @@ function toggleFiltersDisplay() { openFiltersDisplay(); } } -filtersToggleButton && filtersToggleButton.addEventListener("click", toggleFiltersDisplay); -filtersContainer && closeFiltersBtn.addEventListener("click", closeFiltersDisplay); +filtersToggleButton.addEventListener("click", toggleFiltersDisplay); /* Handle submit chosen filters */ const submitFiltersFormHandler = (ev) => { @@ -343,15 +343,15 @@ const submitFiltersFormHandler = (ev) => { filters.attributes = []; - attributeBoxNodes.forEach(e => filters.attributes.push(e.value)); + attributeBoxNodes?.forEach(e => filters.attributes.push(e.value)); filters.kind = []; - kindBoxNodes.forEach(e => filters.kind.push(e.value)); + kindBoxNodes?.forEach(e => filters.kind.push(e.value)); closeFiltersDisplay(); submitSearchFormHandler(ev); }; -filtersForm && filtersForm.addEventListener('submit', submitFiltersFormHandler); +filtersForm.addEventListener('submit', submitFiltersFormHandler); diff --git a/searchWorker.js b/searchWorker.js index 0ca91b6..f2af8b0 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -20,17 +20,21 @@ onconnect = ({ports: [port]}) => port.onmessage = ({ data }) => { const { query, filters, maxCount } = data; const filterFunc = (result) => filterItemResult(result, filters); - const results = miniSearch.search(query, { - boost: { module: 1, description: 2, name: 3 }, - combineWith: 'AND', - filter: filterFunc, - // prefix: (term) => term.length > 3, - // fuzzy: (term) => term.length > 3 && 0.2, - }); - - const response = typeof maxCount === "number" && maxCount >= 0 ? results.slice(0, maxCount) : results; - console.log(response) - port.postMessage({response, total: results.length}); + + if (query && typeof query === "string" && query.length > 0) { + const results = miniSearch.search(query, { + boost: { module: 1, description: 2, name: 3 }, + combineWith: 'AND', + filter: filterFunc, + // prefix: (term) => term.length > 3, + // fuzzy: (term) => term.length > 3 && 0.2, + }); + + const response = typeof maxCount === "number" && maxCount >= 0 ? results.slice(0, maxCount) : results; + console.log(response) + port.postMessage({response, total: results.length}); + } + port.postMessage({response: [], total: 0}); }; const filterItemResult = (result, filters = {}) => { From c01f2303b589103136661a951ead0ee4da2bd02a Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Mon, 17 May 2021 09:38:00 +0300 Subject: [PATCH 23/25] trim query whitespace before searching --- searchWorker.js | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/searchWorker.js b/searchWorker.js index f2af8b0..831b308 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -20,9 +20,9 @@ onconnect = ({ports: [port]}) => port.onmessage = ({ data }) => { const { query, filters, maxCount } = data; const filterFunc = (result) => filterItemResult(result, filters); - - if (query && typeof query === "string" && query.length > 0) { - const results = miniSearch.search(query, { + const sanitizedQuery = query.trim(); + if (sanitizedQuery && typeof sanitizedQuery === "string" && sanitizedQuery.length > 0) { + const results = miniSearch.search(sanitizedQuery, { boost: { module: 1, description: 2, name: 3 }, combineWith: 'AND', filter: filterFunc, From 14355ad97229ac190532f05a96d9dd0816d2214b Mon Sep 17 00:00:00 2001 From: Polina Boneva Date: Mon, 17 May 2021 09:46:28 +0300 Subject: [PATCH 24/25] remove unnecessary files --- import_name.py | 60 -------------------------------------- mathlib_data_structures.py | 53 --------------------------------- 2 files changed, 113 deletions(-) delete mode 100644 import_name.py delete mode 100644 mathlib_data_structures.py diff --git a/import_name.py b/import_name.py deleted file mode 100644 index 26f9e1c..0000000 --- a/import_name.py +++ /dev/null @@ -1,60 +0,0 @@ -import subprocess -from typing import NamedTuple, List -from pathlib import Path -import json -import toml - -class ImportName(NamedTuple): - project: str - parts: List[str] - raw_path: Path - - @classmethod - def of(cls, fname: str): - fname = Path(fname) - path_info = [(p.resolve(), get_name_from_leanpkg_path(p)) for p in lean_paths] - path_details = "".join(f" - {p}\n" for p, _ in path_info) - - for p, name in path_info: - try: - rel_path = fname.relative_to(p) - except ValueError: - pass - else: - return cls(name, rel_path.with_suffix('').parts, fname) - - raise RuntimeError( - f"Cannot determine import name for {fname}; it is not within any of the directories returned by `lean --path`:\n" - f"{path_details}" - f"Did you generate `export.json` using a different Lean installation to the one this script is running with?") - - @property - def name(self): - return '.'.join(self.parts) - - @property - def url(self): - return '/'.join(self.parts) + '.html' - -def get_name_from_leanpkg_path(p: Path) -> str: - """ get the package name corresponding to a source path """ - if p.parts[-5:] == Path('bin/../lib/lean/library').parts or p.parts[-3:] == Path('bin/../library').parts: - return "core" - - # try the toml - p_leanpkg = p / '..' / 'leanpkg.toml' - try: - f = p_leanpkg.open() - except FileNotFoundError: - pass - else: - with f: - parsed_toml = toml.loads(f.read()) - return parsed_toml['package']['name'] - - return '' - -lean_paths = [ - Path(p) - for p in json.loads(subprocess.check_output(['lean', '--path']).decode())['path'] -] diff --git a/mathlib_data_structures.py b/mathlib_data_structures.py deleted file mode 100644 index e296906..0000000 --- a/mathlib_data_structures.py +++ /dev/null @@ -1,53 +0,0 @@ -class mathlibStructures: - DECLARATIONS = 'decls' - TACTICS = 'tactic_docs' - MODULE_DESCRIPTIONS = 'mod_docs' - NOTES = 'notes' - INSTANCES = 'instances' - -class declaration: - NAME = 'name' - IS_META = 'is_meta' - ARGS = 'args' - TYPE = 'type' - DOC_STRING = 'doc_string' - FILENAME = 'filename' - LINE = 'line' - ATTRIBUTES = 'attributes' - EQUATIONS = 'equations' - KIND = 'kind' - STRUCTURE_FIELDS = 'structure_fields' - CONSTRUCTORS = 'constructors' - -class declarationKindsSource: - THEOREM = 'thm' - CONST = 'cnst' - AXIOM = 'ax' - -class declarationKindsDestination: - STRUCTURE = 'structure' - INDUCTIVE = 'inductive' - THEOREM = 'theorem' - CONST = 'const' - AXIOM = 'axiom' - -class tactic: - NAME = 'name' - CATEGORY = 'category' - DECL_NAMES = 'decl_names' - TAGS = 'tags' - DESCRIPTION = 'description' - IMPORT = 'import' - -class tacticCategories: - TACTIC = 'tactic' - COMMAND = 'command' - HOLE_COMMAND = 'hole_command' - ATTRIBUTE = 'attribute' - -class generalPages: - INDEX = 'index' - TACTICS = 'tactics' - COMMANDS = 'commands' - HOLE_COMMANDS = 'hole_commands' - ATTRIBUTES = 'notes' \ No newline at end of file From d71a7dae2eccada406974ac84a0f03cd327e14fa Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 29 Jun 2021 20:49:20 +0200 Subject: [PATCH 25/25] Change extension from .json to .bmp --- print_docs.py | 4 ++-- searchWorker.js | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/print_docs.py b/print_docs.py index e51695c..2cc252d 100644 --- a/print_docs.py +++ b/print_docs.py @@ -765,7 +765,7 @@ def mk_export_searchable_db(file_map, tactic_docs): def write_export_searchable_db(searchable_data): json_str = json.dumps(searchable_data) - with open_outfile('searchable_data.json') as out: + with open_outfile('searchable_data.bmp') as out: out.write(json_str) def main(): @@ -783,4 +783,4 @@ def main(): write_site_map(file_map) if __name__ == '__main__': - main() \ No newline at end of file + main() diff --git a/searchWorker.js b/searchWorker.js index 831b308..2508066 100644 --- a/searchWorker.js +++ b/searchWorker.js @@ -1,7 +1,7 @@ // Access indexed data structure to be used for searching through the documentation const req = new XMLHttpRequest(); -req.open('GET', 'searchable_data.json', false /* blocking */); +req.open('GET', 'searchable_data.bmp', false /* blocking */); req.responseType = 'json'; req.send(); @@ -68,4 +68,4 @@ const filterItemResult = (result, filters = {}) => { hasAttrFilter ? isResultAttrIncluded : isResultKindIncluded; -} \ No newline at end of file +}