Searching the documentation with filters

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 '<unknown>'
+
+lean_paths = [
+  Path(p)
+  for p in json.loads(subprocess.check_output(['lean', '--path']).decode())['path']
+]

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.30.0"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "97d13d7561ef9c9a21587cf62324f8b2d215a7f8"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "87adde497c62a4e4e8fdd0fd5cfc46a2d1bd5371"}

mathlib_data_structures.py

@@ -0,0 +1,53 @@
+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'