Add unsafe filtering in catalog
This commit is contained in:
parent
9f53781ffe
commit
3cb0795bb6
12
Main.lean
12
Main.lean
|
@ -2,6 +2,7 @@ import Lean.Data.Json
|
|||
import Lean.Environment
|
||||
|
||||
import Pantograph.Commands
|
||||
import Pantograph.Symbols
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
|
@ -35,7 +36,12 @@ def create (args: Create): Subroutine CreateResult := do
|
|||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
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 :=
|
||||
let li := s.split (λ c => c == '.')
|
||||
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
|
||||
| .some env =>
|
||||
let names := env.constants.fold (init := []) (λ es name info =>
|
||||
if info.isUnsafe ∨ es.length > 500 then es else (toString name)::es)
|
||||
--let names := env.constants.toList.map (λ ⟨x, _⟩ => toString x)
|
||||
if es.length > 3000 ∨ is_symbol_unsafe_or_internal name info then es else (toString name)::es)
|
||||
return { theorems := names }
|
||||
| .none => throw s!"Invalid environment id {args.id}"
|
||||
|
||||
|
@ -99,5 +104,6 @@ unsafe def loop : T IO Unit := do
|
|||
loop
|
||||
|
||||
unsafe def main : IO Unit := do
|
||||
Lean.enableInitializersExecution
|
||||
Lean.initSearchPath (← Lean.findSysroot)
|
||||
StateT.run' loop ⟨#[]⟩
|
||||
|
|
|
@ -0,0 +1,2 @@
|
|||
import Pantograph.Commands
|
||||
import Pantograph.Symbols
|
|
@ -12,6 +12,8 @@ structure Catalog where
|
|||
|
||||
structure CreateResult where
|
||||
id: Nat
|
||||
symbols: Nat
|
||||
filtered_symbols: Nat
|
||||
deriving Lean.ToJson
|
||||
structure CatalogResult where
|
||||
theorems: List String
|
||||
|
|
|
@ -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
|
12
README.md
12
README.md
|
@ -11,6 +11,8 @@ lake build
|
|||
In order to use `mathlib`, its binary must also be built
|
||||
|
||||
``` sh
|
||||
lake build Qq
|
||||
lake build aesop
|
||||
lake build std
|
||||
lake build mathlib
|
||||
```
|
||||
|
@ -18,11 +20,19 @@ lake build mathlib
|
|||
## Usage
|
||||
|
||||
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
|
||||
{"cmd": "create", "payload": {"imports": ["Mathlib.Analysis.Seminorm"]}}
|
||||
{"cmd": "catalog", "payload": {"id": 0}}
|
||||
```
|
||||
There is temporarily a limit of 500 symbols to prevent stack overflow.
|
||||
|
||||
|
||||
|
||||
|
|
|
@ -2,9 +2,7 @@ import Lake
|
|||
open Lake DSL
|
||||
|
||||
|
||||
package pantograph {
|
||||
-- add package configuration options here
|
||||
}
|
||||
package pantograph
|
||||
|
||||
require mathlib from git
|
||||
"https://github.com/leanprover-community/mathlib4.git" @ "8e5a00a8afc8913c0584cb85f37951995275fd87"
|
||||
|
@ -16,5 +14,6 @@ lean_lib Pantograph {
|
|||
@[default_target]
|
||||
lean_exe pantograph {
|
||||
root := `Main
|
||||
-- Somehow solves the native symbol not found problem
|
||||
supportInterpreter := true
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue