Leni Aniva aniva
  • Stanford University Centaur Lab
  • https://leni.sh
  • Director of NorCal Hakkero Factory No. 1

  • Joined on 2023-08-21
aniva pushed to misc/version at aniva/Pantograph 2024-10-06 16:10:28 -07:00
c3076cbb7d chore: Update Lean to v4.12.0
aniva pushed to misc/version at aniva/Pantograph 2024-10-06 15:52:46 -07:00
aniva created branch misc/version in aniva/Pantograph 2024-10-06 15:52:46 -07:00
aniva pushed to env/catalog at aniva/Pantograph 2024-10-06 15:31:16 -07:00
95be491bbb Merge branch 'dev' into env/catalog
22ddfaaf21 Merge pull request 'feat: Error reporting in frontend' (#107) from frontend/error into dev
d0321e72dd feat: Add message diagnostics to frontend.process
452c390711 Merge pull request 'feat: Collect holes in Lean file and put them into a `GoalState`' (#99) from frontend/collect-holes into dev
10cb32e03f Merge branch 'dev' into frontend/collect-holes
Compare 18 commits »
aniva closed issue aniva/Pantograph#106 2024-10-05 22:40:54 -07:00
Report error when frontend parsing fails
aniva commented on issue aniva/Pantograph#106 2024-10-05 22:40:53 -07:00
Report error when frontend parsing fails

Done #107

aniva pushed to dev at aniva/Pantograph 2024-10-05 22:39:25 -07:00
22ddfaaf21 Merge pull request 'feat: Error reporting in frontend' (#107) from frontend/error into dev
d0321e72dd feat: Add message diagnostics to frontend.process
Compare 2 commits »
aniva deleted branch frontend/error from aniva/Pantograph 2024-10-05 22:39:25 -07:00
aniva merged pull request aniva/Pantograph#107 2024-10-05 22:39:24 -07:00
feat: Error reporting in frontend
aniva pushed to frontend/error at aniva/Pantograph 2024-10-05 14:49:39 -07:00
d0321e72dd feat: Add message diagnostics to frontend.process
aniva pushed to frontend/error at aniva/Pantograph 2024-10-05 14:09:13 -07:00
452c390711 Merge pull request 'feat: Collect holes in Lean file and put them into a `GoalState`' (#99) from frontend/collect-holes into dev
10cb32e03f Merge branch 'dev' into frontend/collect-holes
a03eeddc9b fix: Variable duplication in nested translation
530a1a1a97 fix: Extracting `sorry`s from coupled goals
143cd289bb fix: Extraction of sorry's from nested tactics
Compare 15 commits »
aniva created pull request aniva/Pantograph#107 2024-10-05 10:30:18 -07:00
feat: Error reporting in frontend
aniva pushed to frontend/error at aniva/Pantograph 2024-10-05 10:29:55 -07:00
aniva created branch frontend/error in aniva/Pantograph 2024-10-05 10:29:55 -07:00
aniva pushed to env/catalog at aniva/Pantograph 2024-10-05 10:29:36 -07:00
b9b8265fd5 chore: Remove more thin wrappers
aniva opened issue aniva/Pantograph#106 2024-10-04 22:01:56 -07:00
Report error when frontend parsing fails
aniva created pull request aniva/Pantograph#105 2024-10-04 12:59:16 -07:00
feat: Remove most filters on catalog
aniva pushed to env/catalog at aniva/Pantograph 2024-10-04 12:59:02 -07:00
3c808506c1 feat: Remove most filters on catalog
aniva created branch env/catalog in aniva/Pantograph 2024-10-04 12:59:02 -07:00
aniva pushed to ui/fish at aniva/config 2024-10-03 17:56:16 -07:00
b9a1bf3dd3 feat: Set bg color to differentiate prompt