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 pushed to bug/core-state-error-linger at aniva/Pantograph 2024-12-11 09:06:52 -08:00
396a787771 feat: Reset message log in MainM
aniva pushed to bug/core-state-error-linger at aniva/Pantograph 2024-12-11 09:05:55 -08:00
ab77418e24 fix: Drop previous message lists
aniva pushed to bug/core-state-error-linger at aniva/Pantograph 2024-12-11 09:02:33 -08:00
f2f71a6028 fix: Reset core message log
aniva created branch bug/core-state-error-linger in aniva/Pantograph 2024-12-11 09:02:33 -08:00
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 created branch lib/export in aniva/Pantograph 2024-12-11 01:27:18 -08:00
aniva pushed to lib/export at 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 »