diff --git a/leanpkg.toml b/leanpkg.toml
index 623b961..73994c2 100644
--- a/leanpkg.toml
+++ b/leanpkg.toml
@@ -1,8 +1,8 @@
[package]
name = "."
version = "0.1"
-lean_version = "leanprover-community/lean:3.10.0"
+lean_version = "leanprover-community/lean:3.13.2"
path = "src"
[dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "4503f8fe2ab79301730e796be2899f234acca0e0"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "1f00282972fcf8957c3d4b4ecac0601dd7550355"}
diff --git a/print_docs.py b/print_docs.py
index ba37618..4ad7314 100644
--- a/print_docs.py
+++ b/print_docs.py
@@ -99,6 +99,27 @@ def library_link(filename, line=None):
else mathlib_github_src_root + filename.split('mathlib/src/', 1)[1]
return root + ('#L' + str(line) if line is not None else '')
+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 nav_link(filename):
tks = filename_core('', filename, '').split('/')
links = ['root'.format(site_root)]
@@ -646,6 +667,24 @@ def write_site_map(partition):
out.write(site_root + filename + '.html\n')
out.close()
+def write_docs_redirect(decl_name, decl_loc):
+ out = open_outfile(html_root + 'find/' + decl_name + '/index.html', 'w')
+ url = filename_core(site_root, decl_loc, 'html')
+ out.write(f'')
+ out.close()
+
+def write_src_redirect(decl_name, decl_loc, file_map):
+ out = open_outfile(html_root + 'find/' + decl_name + '/src/index.html', 'w')
+ url = library_link_from_decl_name(decl_name, decl_loc, file_map)
+ out.write(f'')
+ out.close()
+
+def write_redirects(loc_map, file_map):
+ for decl_name in loc_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 cp(a, b):
if use_symlinks:
@@ -657,7 +696,10 @@ def cp(a, b):
cp('style_js_frame.css', path+'style_js_frame.css')
cp('nav.js', path+'nav.js')
+
+
file_map, loc_map, notes, mod_docs, instances, tactic_docs = load_json()
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)
write_site_map(file_map)