Add unsafe filtering in catalog

This commit is contained in:
Leni Aniva 2023-05-12 16:12:21 -07:00
parent 7c96479bb5
commit d3af535652
6 changed files with 44 additions and 7 deletions

View File

@ -2,6 +2,7 @@ import Lean.Data.Json
import Lean.Environment import Lean.Environment
import Pantograph.Commands import Pantograph.Commands
import Pantograph.Symbols
namespace Pantograph namespace Pantograph
@ -35,7 +36,12 @@ def create (args: Create): Subroutine CreateResult := do
(opts := {}) (opts := {})
(trustLevel := 1) (trustLevel := 1)
modify fun s => { environments := s.environments.push env } modify fun s => { environments := s.environments.push env }
return { id := id } let num_filtered_symbols := env.constants.fold (init := 0) (λ acc name info =>
acc + if is_symbol_unsafe_or_internal name info then 0 else 1)
return {
id := id,
symbols := env.constants.size,
filtered_symbols := num_filtered_symbols }
where strTransform (s: String): Lean.Import := where strTransform (s: String): Lean.Import :=
let li := s.split (λ c => c == '.') let li := s.split (λ c => c == '.')
let name := li.foldl (λ pre segment => Lean.Name.str pre segment) Lean.Name.anonymous let name := li.foldl (λ pre segment => Lean.Name.str pre segment) Lean.Name.anonymous
@ -46,8 +52,7 @@ def catalog (args: Catalog): Subroutine CatalogResult := do
match state.environments.get? args.id with match state.environments.get? args.id with
| .some env => | .some env =>
let names := env.constants.fold (init := []) (λ es name info => let names := env.constants.fold (init := []) (λ es name info =>
if info.isUnsafe es.length > 500 then es else (toString name)::es) if es.length > 3000 is_symbol_unsafe_or_internal name info then es else (toString name)::es)
--let names := env.constants.toList.map (λ ⟨x, _⟩ => toString x)
return { theorems := names } return { theorems := names }
| .none => throw s!"Invalid environment id {args.id}" | .none => throw s!"Invalid environment id {args.id}"
@ -99,5 +104,6 @@ unsafe def loop : T IO Unit := do
loop loop
unsafe def main : IO Unit := do unsafe def main : IO Unit := do
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot) Lean.initSearchPath (← Lean.findSysroot)
StateT.run' loop ⟨#[]⟩ StateT.run' loop ⟨#[]⟩

2
Pantograph.lean Normal file
View File

@ -0,0 +1,2 @@
import Pantograph.Commands
import Pantograph.Symbols

View File

@ -12,6 +12,8 @@ structure Catalog where
structure CreateResult where structure CreateResult where
id: Nat id: Nat
symbols: Nat
filtered_symbols: Nat
deriving Lean.ToJson deriving Lean.ToJson
structure CatalogResult where structure CatalogResult where
theorems: List String theorems: List String

18
Pantograph/Symbols.lean Normal file
View File

@ -0,0 +1,18 @@
/-
- Manages the visibility status of symbols
-/
import Lean.Declaration
namespace Pantograph
def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
let nameDeduce: Bool := match n.getRoot with
| .str _ name => name.startsWith "_" name == "Lean"
| _ => true
let stemDeduce: Bool := match n with
| .anonymous => true
| .str _ name => name.startsWith "_"
| .num _ _ => true
nameDeduce stemDeduce info.isUnsafe
end Pantograph

View File

@ -11,6 +11,8 @@ lake build
In order to use `mathlib`, its binary must also be built In order to use `mathlib`, its binary must also be built
``` sh ``` sh
lake build Qq
lake build aesop
lake build std lake build std
lake build mathlib lake build mathlib
``` ```
@ -18,11 +20,19 @@ lake build mathlib
## Usage ## Usage
The binary must be run inside a `lake env` environment. The binary must be run inside a `lake env` environment.
Example: (~5k symbols)
```
$ lake env build/bin/Pantograph
{"cmd": "create", "payload": {"imports": ["Init"]}}
{"cmd": "catalog", "payload": {"id": 0}}
```
Example with `mathlib` (~90k symbols)
``` ```
$ lake env build/bin/Pantograph $ lake env build/bin/Pantograph
{"cmd": "create", "payload": {"imports": ["Mathlib.Analysis.Seminorm"]}} {"cmd": "create", "payload": {"imports": ["Mathlib.Analysis.Seminorm"]}}
{"cmd": "catalog", "payload": {"id": 0}} {"cmd": "catalog", "payload": {"id": 0}}
``` ```
There is temporarily a limit of 500 symbols to prevent stack overflow.

View File

@ -2,9 +2,7 @@ import Lake
open Lake DSL open Lake DSL
package pantograph { package pantograph
-- add package configuration options here
}
require mathlib from git require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "8e5a00a8afc8913c0584cb85f37951995275fd87" "https://github.com/leanprover-community/mathlib4.git" @ "8e5a00a8afc8913c0584cb85f37951995275fd87"
@ -16,5 +14,6 @@ lean_lib Pantograph {
@[default_target] @[default_target]
lean_exe pantograph { lean_exe pantograph {
root := `Main root := `Main
-- Somehow solves the native symbol not found problem
supportInterpreter := true supportInterpreter := true
} }