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
12
 Projects Packages Public Activity Starred Repositories
9
aniva commented on pull request aniva/Pantograph#111 2024-10-12 16:54:06 -07:00
feat: Let tactic in REPL

Testing seems fine. Approved.

aniva created pull request aniva/Pantograph#113 2024-10-12 16:53:35 -07:00
feat: Capture environment in drafting
aniva pushed to frontend/environment at aniva/Pantograph 2024-10-12 16:52:42 -07:00
946e688dec test(frontend): Environment capture
aniva pushed to frontend/environment at aniva/Pantograph 2024-10-12 16:50:30 -07:00
5a2ae880f4 feat: Capture environment in drafting
aniva created branch frontend/environment in aniva/Pantograph 2024-10-12 16:50:30 -07:00
aniva opened issue aniva/Pantograph#112 2024-10-12 16:38:31 -07:00
feat: Enable environment capture during frontend.process
aniva created pull request aniva/Pantograph#111 2024-10-12 16:18:04 -07:00
feat: Let tactic in REPL
aniva created branch repl/tactic-let in aniva/Pantograph 2024-10-12 16:17:33 -07:00
aniva pushed to repl/tactic-let at aniva/Pantograph 2024-10-12 16:17:33 -07:00
645d9c9250 feat: Let tactic in REPL
aniva pushed tag v0.2.19-alpha to aniva/Pantograph 2024-10-09 18:09:56 -07:00
aniva pushed to dev at aniva/Pantograph 2024-10-09 18:08:11 -07:00
e0ba65a7cd Merge pull request 'fix: Delayed MVars in MetaTranslate' (#110) from bug/frontend-translate-delayed-mvar into dev
641f8c3883 fix: Translate level mvars
0bac4fdecd Merge branch 'dev' into bug/frontend-translate-delayed-mvar
0e8c9f890b fix: Translate fvars in pending context
420e863756 fix: Delayed mvars in MetaTranslate
Compare 5 commits »
aniva deleted branch bug/frontend-translate-delayed-mvar from aniva/Pantograph 2024-10-09 18:08:11 -07:00
aniva merged pull request aniva/Pantograph#110 2024-10-09 18:08:10 -07:00
fix: Delayed MVars in MetaTranslate
aniva pushed to bug/frontend-translate-delayed-mvar at aniva/Pantograph 2024-10-09 15:49:48 -07:00
641f8c3883 fix: Translate level mvars
aniva commented on pull request aniva/Pantograph#110 2024-10-08 23:56:00 -07:00
fix: Delayed MVars in MetaTranslate

This seems to fix it based on experimental results from https://github.com/lenianiva/PyPantograph/pull/21.

I don't know how to write unit tests for this bug.

aniva pushed to bug/frontend-translate-delayed-mvar at aniva/Pantograph 2024-10-08 23:54:01 -07:00
0bac4fdecd Merge branch 'dev' into bug/frontend-translate-delayed-mvar
1cd41b4993 Merge pull request 'feat: Catch and print IO errors in REPL' (#109) from repl/io-exception into dev
f03c47207b Merge branch 'dev' into repl/io-exception
1f4f2d7d6d Merge pull request 'chore: Update Lean to v4.12.0' (#108) from misc/version into dev
Compare 4 commits »
aniva deleted branch repl/io-exception from aniva/Pantograph 2024-10-08 23:50:38 -07:00
aniva pushed to dev at aniva/Pantograph 2024-10-08 23:50:38 -07:00
1cd41b4993 Merge pull request 'feat: Catch and print IO errors in REPL' (#109) from repl/io-exception into dev
f03c47207b Merge branch 'dev' into repl/io-exception
05d0b7739a feat: Catch IO errors in json format
5e776a1b49 feat: Catch and print IO errors
Compare 4 commits »
aniva merged pull request aniva/Pantograph#109 2024-10-08 23:50:37 -07:00
feat: Catch and print IO errors in REPL
aniva pushed to repl/io-exception at aniva/Pantograph 2024-10-08 23:49:59 -07:00
f03c47207b Merge branch 'dev' into repl/io-exception
1f4f2d7d6d Merge pull request 'chore: Update Lean to v4.12.0' (#108) from misc/version into dev
Compare 2 commits »