Commit Graph

Select branches

Hide Pull Requests

dev

frontend/data

goal/tactic

main

misc/build

misc/interaction

misc/toolchain

parse/level

serial/pickle

#10

#100

#101

#105

#107

#108

#109

#11

#110

#111

#113

#115

#116

#119

#12

#120

#13

#14

#15

#16

#17

#2

#20

#21

#25

#26

#27

#28

#29

#30

#31

#32

#33

#35

#36

#37

#38

#40

#41

#42

#43

#44

#45

#46

#47

#48

#49

#5

#50

#51

#52

#53

#54

#55

#56

#58

#59

#60

#63

#64

#65

#66

#68

#69

#7

#70

#71

#72

#73

#75

#76

#79

#81

#82

#83

#85

#86

#87

#89

#90

#91

#92

#94

#96

#99

0.1

0.2.3

v0.2.10

v0.2.10-alpha

v0.2.11

v0.2.12

v0.2.13

v0.2.14

v0.2.18

v0.2.19

v0.2.19-alpha

v0.2.5

v0.2.6

v0.2.7

v0.2.8

v0.2.9

Mono Color

• 77b577d0e3
  
  Merge branch 'dev' into frontend/data frontend/data Leni Aniva 2024-11-08 14:52:03 -0800
• 495ea1ac14
  
  feat: Environment pickling serial/pickle Leni Aniva 2024-11-08 14:49:49 -0800
• ee8063e1f5
  
  refactor: Merge all Delation functions Leni Aniva 2024-11-08 14:41:24 -0800
• 70f86f6e93
  
  doc: Update delation documentation Leni Aniva 2024-11-08 14:34:15 -0800
• 0d57027681
  
  refactor: Merge Condensed into Delate Leni Aniva 2024-11-08 13:05:48 -0800
• 1c4f38e5eb
  
  refactor: Rename {Serial,Delate}.lean Leni Aniva 2024-11-08 13:04:00 -0800
• d7c9590780
  
  feat: Extract used constants from invocation Leni Aniva 2024-11-05 14:37:06 -0800
• b99fecdb50
  
  chore: Update `lean4-nix` misc/build Leni Aniva 2024-10-26 17:52:37 -0700
• 23efed960b
  
  chore: Update `lean4-nix` Leni Aniva 2024-10-26 13:49:03 -0700
• 8fe4c78c2a
  
  doc: Change license to Apache2 dev Leni Aniva 2024-10-21 09:59:13 -0700
• d23f99fd44
  
  feat: Update Lean4 upstream to unofficial flake Leni Aniva 2024-10-14 21:16:41 -0700
• a11127a64e Merge pull request 'feat: Capture environment in drafting' (#113) from frontend/environment into dev v0.2.19 Leni Aniva 2024-10-12 16:59:41 -0700
• 72e41e1e1e
  
  Merge branch 'dev' into frontend/environment Leni Aniva 2024-10-12 16:57:55 -0700
• 5b278d68d4 Merge pull request 'feat: Let tactic in REPL' (#111) from repl/tactic-let into dev Leni Aniva 2024-10-12 16:54:12 -0700
• 946e688dec
  
  test(frontend): Environment capture Leni Aniva 2024-10-12 16:52:36 -0700
• 5a2ae880f4
  
  feat: Capture environment in drafting Leni Aniva 2024-10-12 16:46:44 -0700
• 645d9c9250
  
  feat: Let tactic in REPL Leni Aniva 2024-10-12 16:17:21 -0700
• e0ba65a7cd Merge pull request 'fix: Delayed MVars in MetaTranslate' (#110) from bug/frontend-translate-delayed-mvar into dev v0.2.19-alpha Leni Aniva 2024-10-09 18:08:09 -0700
• 641f8c3883
  
  fix: Translate level mvars Leni Aniva 2024-10-09 15:49:10 -0700
• 0bac4fdecd
  
  Merge branch 'dev' into bug/frontend-translate-delayed-mvar Leni Aniva 2024-10-08 23:53:57 -0700
• 1cd41b4993 Merge pull request 'feat: Catch and print IO errors in REPL' (#109) from repl/io-exception into dev Leni Aniva 2024-10-08 23:50:36 -0700
• f03c47207b
  
  Merge branch 'dev' into repl/io-exception Leni Aniva 2024-10-08 23:49:51 -0700
• 0e8c9f890b
  
  fix: Translate fvars in pending context Leni Aniva 2024-10-08 14:28:35 -0700
• 420e863756
  
  fix: Delayed mvars in MetaTranslate Leni Aniva 2024-10-08 10:32:16 -0700
• 1f4f2d7d6d Merge pull request 'chore: Update Lean to v4.12.0' (#108) from misc/version into dev Leni Aniva 2024-10-08 09:49:08 -0700
• 05d0b7739a
  
  feat: Catch IO errors in json format Leni Aniva 2024-10-08 00:45:45 -0700
• 5e776a1b49
  
  feat: Catch and print IO errors Leni Aniva 2024-10-08 00:17:31 -0700
• 2e1276c21c
  
  chore: Update LSpec dependency Leni Aniva 2024-10-08 00:15:30 -0700
• c3494edc75
  
  fix: Flake build Leni Aniva 2024-10-06 16:46:39 -0700
• 25dd1a32ba
  
  Merge branch 'dev' into misc/version Leni Aniva 2024-10-06 16:12:36 -0700
• 9119f47a8f chore: Remove more thin wrappers Leni Aniva 2024-10-05 10:29:20 -0700
• 8d774d3281 feat: Remove most filters on catalog Leni Aniva 2024-10-04 12:58:16 -0700
• c3076cbb7d
  
  chore: Update Lean to v4.12.0 Leni Aniva 2024-10-06 16:10:18 -0700
• 95be491bbb
  
  Merge branch 'dev' into env/catalog Leni Aniva 2024-10-06 14:25:48 -0700
• 22ddfaaf21 Merge pull request 'feat: Error reporting in frontend' (#107) from frontend/error into dev Leni Aniva 2024-10-05 22:39:23 -0700
• d0321e72dd
  
  feat: Add message diagnostics to frontend.process Leni Aniva 2024-10-05 14:49:17 -0700
• b9b8265fd5
  
  chore: Remove more thin wrappers Leni Aniva 2024-10-05 10:29:20 -0700
• 3c808506c1
  
  feat: Remove most filters on catalog Leni Aniva 2024-10-04 12:58:16 -0700
• 452c390711 Merge pull request 'feat: Collect holes in Lean file and put them into a `GoalState`' (#99) from frontend/collect-holes into dev Leni Aniva 2024-10-03 15:43:00 -0700
• 10cb32e03f
  
  Merge branch 'dev' into frontend/collect-holes Leni Aniva 2024-10-03 11:47:38 -0700
• a03eeddc9b
  
  fix: Variable duplication in nested translation Leni Aniva 2024-10-03 11:46:09 -0700
• 530a1a1a97
  
  fix: Extracting `sorry`s from coupled goals Leni Aniva 2024-10-03 11:35:54 -0700
• b174b4ea79 Merge pull request 'fix: Tactics should produce `.syntheticOpaque` goals' (#100) from goal/tactic into dev Leni Aniva 2024-10-03 08:47:30 -0700
• ed1f96d7f7
  
  Merge branch 'dev' into goal/tactic goal/tactic Leni Aniva 2024-10-03 01:38:10 -0700
• 143cd289bb
  
  fix: Extraction of sorry's from nested tactics Leni Aniva 2024-10-03 01:29:46 -0700
• 18cd1d0388
  
  fix: Extracting sorrys from sketches Leni Aniva 2024-10-02 22:22:20 -0700
• bec84f857b
  
  fix: repl build failure Leni Aniva 2024-09-09 18:43:34 -0700
• fe8b259e4f
  
  feat: Set root when there's just one mvar Leni Aniva 2024-09-09 17:37:59 -0700
• f729a357b9
  
  Merge branch 'dev' into frontend/collect-holes Leni Aniva 2024-09-09 17:35:10 -0700
• 9075ded885
  
  feat: Set `automaticMode` to true by default Leni Aniva 2024-09-09 17:29:43 -0700
• 9f0de0957e
  
  doc: Update documentation for frontend command Leni Aniva 2024-09-09 12:39:32 -0700
• 762a139e78
  
  feat: Export frontend functions Leni Aniva 2024-09-09 12:30:32 -0700
• 4f5950ed78
  
  feat: Convert holes to goals Leni Aniva 2024-09-09 12:26:46 -0700
• 08fb53c020
  
  test: Frontend process testing Leni Aniva 2024-09-09 10:18:20 -0700
• 8e3241c02a
  
  refactor: Move all frontend functions to `Frontend` Leni Aniva 2024-09-08 15:02:43 -0700
• 5e99237e09
  
  fix: Tactics should produce `.syntheticOpaque` goals Leni Aniva 2024-09-08 14:13:39 -0700
• 860344f9c5
  
  refactor: Factor out `FrontendM` driver Leni Aniva 2024-09-08 13:44:46 -0700
• 27e4e45418 Merge pull request 'feat: Automatic Mode' (#92) from goal/automatic into dev v0.2.18 Leni Aniva 2024-09-08 12:25:06 -0700
• b645d79fda
  
  Merge branch 'dev' into goal/automatic Leni Aniva 2024-09-08 12:13:42 -0700
• e36954a589 Merge pull request 'feat: Expose `GoalState` functions' (#94) from lib/export into dev Leni Aniva 2024-09-08 12:10:46 -0700
• 414f1c70fd
  
  Merge branch 'dev' into lib/export Leni Aniva 2024-09-08 12:01:02 -0700
• 25bb964604
  
  test: Automatic mode testing Leni Aniva 2024-09-08 11:57:39 -0700
• 7c49fcff27
  
  refactor: Un-export two field accessor functions Leni Aniva 2024-09-08 11:53:10 -0700
• f11c5ebaa3
  
  doc: Add GPL License Leni Aniva 2024-09-07 14:11:04 -0700
• e4d53733d0
  
  feat: Simplify repl Leni Aniva 2024-09-07 14:03:29 -0700
• 68dac4c951
  
  chore: Version bump to 0.2.18 Leni Aniva 2024-09-07 13:55:41 -0700
• 4042ec707e
  
  refactor: Use `Meta.mapMetaM` Leni Aniva 2024-09-07 13:54:52 -0700
• 8394e1b468
  
  feat: Expose `conv` and `calc` tactics Leni Aniva 2024-09-07 13:47:55 -0700
• 9b3eef35ec
  
  fix: Forgot to include the current goals in resume Leni Aniva 2024-09-06 22:22:19 -0700
• a7b30af36b
  
  refactor: Refactor REPL out of main library Leni Aniva 2024-09-06 22:01:36 -0700
• e2ad6ce6b3
  
  doc: Documentation for automatic mode Leni Aniva 2024-09-06 21:32:02 -0700
• 37473b3efb
  
  feat: Automatic mode (auto resume) Leni Aniva 2024-09-06 21:30:11 -0700
• 82d99ccf9b
  
  refactor: Use `MVarId` across the board Leni Aniva 2024-09-06 21:07:12 -0700
• 02556f3c79
  
  feat: Expose `GoalState` functions Leni Aniva 2024-09-05 11:56:06 -0700
• 9c40a83956
  
  fix: Instantiate type when detecting `eq` Leni Aniva 2024-09-03 19:05:16 -0700
• f8df2599f9
  
  fix: Use `replaceMainGoal` instead of `setGoals` Leni Aniva 2024-09-03 14:18:47 -0700
• 8d2cd6dfc7
  
  fix: Bindings in prograde tactics Leni Aniva 2024-09-03 14:15:52 -0700
• 948b535b5d Merge pull request 'feat: Prograde tactics' (#83) from tactic/eval into dev Leni Aniva 2024-08-31 20:04:38 -0700
• edec0f5733
  
  feat: Use CoreM for diag monad Leni Aniva 2024-08-26 13:42:14 -0400
• 0c529c5cd9
  
  Merge branch 'misc/test-driver' into tactic/eval Leni Aniva 2024-08-18 12:24:26 -0700
• 76765c913c
  
  test: Use `lake test`. Retired `Makefile` Leni Aniva 2024-08-18 12:22:59 -0700
• 3733c10a4e
  
  refactor: Unify call convention Leni Aniva 2024-08-17 16:47:21 -0700
• 5d43068ec3
  
  fix: Flake check failure Leni Aniva 2024-08-17 02:07:17 -0700
• f87eed817f
  
  build: Move non-package output to legacyPackages Leni Aniva 2024-08-17 01:59:48 -0700
• 43e11f1ba3
  
  refactor: Always display isInaccessible Leni Aniva 2024-08-17 00:53:38 -0700
• 0c469027c6
  
  fix: Refactor mvar collection in assign tactic Leni Aniva 2024-08-17 00:50:02 -0700
• e1b7eaab12
  
  fix: Let tactic not bringing binder into scope Leni Aniva 2024-08-17 00:47:12 -0700
• d17b21e282
  
  fix: Use `getMVarsNoDelayed` Leni Aniva 2024-08-16 00:32:34 -0700
• 5b4f8a37eb
  
  refactor: All Tactic/ tactics into MetaM form Leni Aniva 2024-08-15 23:41:17 -0700
• 1e7a186bb1
  
  refactor: MetaM form of define (evaluate) Leni Aniva 2024-08-15 23:23:17 -0700
• 9b0456a5e0
  
  refactor: MetaM form of have and let Leni Aniva 2024-08-15 23:17:15 -0700
• 7968072097
  
  refactor: Remove the newMVarSet mechanism Leni Aniva 2024-08-15 22:53:42 -0700
• e07f9d9b3f
  
  Merge branch 'dev' into tactic/eval Leni Aniva 2024-08-15 22:45:43 -0700
• 56100a30af Merge pull request 'feat: Condensed interface' (#85) from serial/expr into dev Leni Aniva 2024-08-15 22:41:58 -0700
• e943a4b065
  
  refactor: Assign into its own tactic Leni Aniva 2024-08-15 22:39:40 -0700
• 0bc7bc5856
  
  refactor: Remove export of Lean functions Leni Aniva 2024-08-14 01:20:56 -0700
• caac70f0cf
  
  feat: Move non package outputs to dependencies Leni Aniva 2024-08-04 17:52:36 -0700
• 64269868d5
  
  feat: Expose project and leanPkgs in flake Leni Aniva 2024-08-04 17:32:20 -0700
• c9ee31bbfd
  
  feat: Export `mkFun` Leni Aniva 2024-08-02 22:33:03 -0700
• 394fb73137
  
  feat: Add direct expression to string Leni Aniva 2024-08-02 22:00:27 -0700