Leni Aniva aniva
0 Followers · 1 Following
  • Stanford University Centaur Lab
  • https://leni.sh

  • Director of NorCal Hakkero Factory No. 1

  • Joined on 2023-08-21
Repositories
13
 Projects Packages Public Activity Starred Repositories
9
aniva pushed tag v0.2.22 to aniva/Pantograph 2024-12-11 01:28:40 -08:00
aniva deleted branch lib/export from aniva/Pantograph 2024-12-11 01:28:01 -08:00
aniva pushed to lib/export at aniva/Pantograph 2024-12-11 01:27:18 -08:00
aniva created branch lib/export in aniva/Pantograph 2024-12-11 01:27:18 -08:00
aniva commented on issue aniva/Pantograph#126 2024-12-11 01:26:00 -08:00
Extraction of new symbols in each compilation unit

Done #128

aniva closed issue aniva/Pantograph#126 2024-12-11 01:26:00 -08:00
Extraction of new symbols in each compilation unit
aniva commented on issue aniva/Pantograph#125 2024-12-11 01:25:53 -08:00
Wrong code/Compilation Failure Extraction

Done #128

aniva closed issue aniva/Pantograph#125 2024-12-11 01:25:53 -08:00
Wrong code/Compilation Failure Extraction
aniva pushed to dev at aniva/Pantograph 2024-12-11 01:25:37 -08:00
5d76626912 Merge pull request 'feat: Extract type error and new constants' (#128) from frontend/infotree into dev
7cba8efd54 Merge branch 'dev' into frontend/infotree
95503c45e4 doc: frontend.process newConstants
681c3fb78d fix: Disallow indeterminant type `sorry`
37a5884be4 fix: Use `ppSyntax` instead of `ppTactic`
Compare 18 commits »
aniva deleted branch frontend/infotree from aniva/Pantograph 2024-12-11 01:25:37 -08:00
aniva merged pull request aniva/Pantograph#128 2024-12-11 01:25:36 -08:00
feat: Extract type error and new constants
aniva closed issue aniva/Pantograph#122 2024-12-11 01:25:36 -08:00
Mathlib4 Parsing Error
aniva commented on issue aniva/Pantograph#102 2024-12-11 01:16:38 -08:00
Timeout for tactics

https://github.com/leanprover/lean4/issues/3812

aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-11 01:14:49 -08:00
7cba8efd54 Merge branch 'dev' into frontend/infotree
e9fbce7b4d Merge pull request 'fix: Tactic failure on synthesizing placeholder' (#139) from bug/tactic-failure-placeholder into dev
4217dbcf80 Merge branch 'dev' into bug/tactic-failure-placeholder
c96df2ed1c chore: Add `aarch64` build targets to flake
aa122b2bb9 doc: Update rationale link
Compare 14 commits »
aniva deleted branch bug/tactic-failure-placeholder from aniva/Pantograph 2024-12-11 01:13:17 -08:00
aniva pushed to dev at aniva/Pantograph 2024-12-11 01:13:16 -08:00
e9fbce7b4d Merge pull request 'fix: Tactic failure on synthesizing placeholder' (#139) from bug/tactic-failure-placeholder into dev
4217dbcf80 Merge branch 'dev' into bug/tactic-failure-placeholder
aa122b2bb9 doc: Update rationale link
58956d33fe doc: Update behaviour rationale
cb87fcd9dd fix: Insert `mvarDeps`
Compare 11 commits »
aniva merged pull request aniva/Pantograph#139 2024-12-11 01:13:15 -08:00
fix: Tactic failure on synthesizing placeholder
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-11 01:08:53 -08:00
4217dbcf80 Merge branch 'dev' into bug/tactic-failure-placeholder
c96df2ed1c chore: Add `aarch64` build targets to flake
e9cbc6eab3 chore: Update version
Compare 3 commits »
aniva commented on pull request aniva/Pantograph#139 2024-12-11 00:49:13 -08:00
fix: Tactic failure on synthesizing placeholder

Fixed some more problems. Two test cases in Mathlib:

To reproduce, use these files and pipe them into pantograph-repl's stdin.

frontend.process {"file": "theorem amc12a_2021_p12 (a b c…
aniva deleted branch chore/flake from aniva/Pantograph 2024-12-11 00:30:21 -08:00