Commit Graph

Select branches

Hide Pull Requests

dev

main

#10

#100

#101

#105

#107

#108

#109

#11

#110

#111

#113

#115

#116

#119

#12

#120

#121

#123

#128

#129

#13

#130

#133

#134

#135

#136

#139

#14

#140

#141

#143

#144

#145

#146

#148

#149

#15

#152

#153

#154

#155

#156

#157

#158

#159

#16

#161

#164

#165

#166

#168

#169

#17

#172

#173

#174

#176

#177

#178

#179

#181

#182

#183

#185

#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.20

v0.2.21

v0.2.22

v0.2.23

v0.2.24

v0.2.25

v0.2.5

v0.2.6

v0.2.7

v0.2.8

v0.2.9

Mono Color

• ef4e5ecbf8
  
  chore: Update version v0.2.24 Leni Aniva 2025-01-10 12:55:26 -0800
• a374af3a5f Merge pull request 'fix: Incorrect binder capture' (#152) from bug/incorrect-binder-capture into dev Leni Aniva 2025-01-10 12:49:14 -0800
• 9eec14503a
  
  Merge branch 'dev' into bug/incorrect-binder-capture Leni Aniva 2025-01-10 12:48:18 -0800
• 814f36eb63 Merge pull request 'feat: Add source location extraction' (#154) from env/inspect into dev Leni Aniva 2025-01-10 12:47:35 -0800
• 4a4b02d7b0
  
  test: Source location extraction Leni Aniva 2025-01-10 12:47:13 -0800
• 97eaadc93c
  
  feat: Add source location extraction Leni Aniva 2025-01-10 12:16:23 -0800
• aa066b8634
  
  fix: Add test Leni Aniva 2025-01-08 22:53:10 -0800
• 072d351f04
  
  fix: Delete extraneous test Leni Aniva 2025-01-08 22:47:08 -0800
• cb46b47a60
  
  test: Draft tactic test Leni Aniva 2025-01-08 22:23:30 -0800
• 5ce6123de7
  
  feat: Draft tactic Leni Aniva 2025-01-08 19:56:14 -0800
• f891960362
  
  fix: Volatile test Leni Aniva 2025-01-07 17:52:28 -0800
• 6302b747b8
  
  feat: Improve error message clarity Leni Aniva 2025-01-07 17:51:32 -0800
• 07e737eb81 Merge pull request 'feat: Simplify sexp printing' (#149) from delate/sexp into dev Leni Aniva 2025-01-07 17:31:29 -0800
• 56f40462ae Merge pull request 'fix: Unnecessary instantiation call' (#148) from goal/tactic into dev Leni Aniva 2025-01-07 17:31:08 -0800
• 524314721b
  
  feat: Gate type error collection behind flag Leni Aniva 2025-01-07 19:40:03 +0900
• 5a05e9e8d4
  
  test: Add binder capturing test Leni Aniva 2024-12-22 08:47:38 +0900
• 48b924fae2
  
  fix(frontend): Incorrect capture of binder term Leni Aniva 2024-12-20 19:10:38 +0900
• b42d917aa7
  
  fix: Unnecessary instantiation call Leni Aniva 2024-12-17 08:18:27 +0900
• 53bad1c4c9
  
  refactor: Remove obsolete sanitize option Leni Aniva 2024-12-15 12:52:08 -0800
• 7a3b89cc0e
  
  feat: Simplify sexp binder Leni Aniva 2024-12-15 12:48:49 -0800
• c0090dec97
  
  fix: Quote string literal in sexp Leni Aniva 2024-12-15 12:40:47 -0800
• 13e01b9e62
  
  Merge branch 'dev' into misc/version Leni Aniva 2024-12-11 20:51:17 -0800
• 3744cfaa96 Merge pull request 'feat: Print value of arbitrary mvar and goals in goal state' (#141) from goal/print into dev v0.2.23 Leni Aniva 2024-12-11 16:52:19 -0800
• 0fa57a5a15
  
  Merge branch 'dev' into goal/print Leni Aniva 2024-12-11 16:51:58 -0800
• b9c114fe21 Merge pull request 'doc: Add limitations' (#145) from doc/rationale into dev Leni Aniva 2024-12-11 16:51:23 -0800
• 2f732a7f20
  
  feat: Print goals in `goal.print` Leni Aniva 2024-12-11 16:49:52 -0800
• eeb336c944
  
  Merge branch 'dev' into goal/print Leni Aniva 2024-12-11 16:40:01 -0800
• bb445f4d73
  
  chore: Update version Leni Aniva 2024-12-11 16:38:59 -0800
• f111da7de7
  
  doc: Add limitations Leni Aniva 2024-12-11 15:09:14 -0800
• fecab387dc
  
  merge: branch 'dev' into doc/rationale Leni Aniva 2024-12-11 15:05:09 -0800
• f14a37897b Merge pull request 'fix: Reset core message log' (#144) from bug/core-state-error-linger into dev v0.2.22 Leni Aniva 2024-12-11 09:09:33 -0800
• 396a787771
  
  feat: Reset message log in MainM Leni Aniva 2024-12-11 09:06:42 -0800
• ab77418e24
  
  fix: Drop previous message lists Leni Aniva 2024-12-11 09:05:47 -0800
• f2f71a6028
  
  fix: Reset core message log Leni Aniva 2024-12-11 09:01:57 -0800
• 5d76626912 Merge pull request 'feat: Extract type error and new constants' (#128) from frontend/infotree into dev Leni Aniva 2024-12-11 01:25:35 -0800
• 7cba8efd54
  
  Merge branch 'dev' into frontend/infotree Leni Aniva 2024-12-11 01:14:15 -0800
• e9fbce7b4d Merge pull request 'fix: Tactic failure on synthesizing placeholder' (#139) from bug/tactic-failure-placeholder into dev Leni Aniva 2024-12-11 01:13:14 -0800
• 4217dbcf80
  
  Merge branch 'dev' into bug/tactic-failure-placeholder Leni Aniva 2024-12-11 01:08:44 -0800
• c96df2ed1c
  
  chore: Add `aarch64` build targets to flake Leni Aniva 2024-12-11 00:29:29 -0800
• aa122b2bb9
  
  doc: Update rationale link Leni Aniva 2024-12-11 00:24:56 -0800
• 58956d33fe
  
  doc: Update behaviour rationale Leni Aniva 2024-12-11 00:21:26 -0800
• cb87fcd9dd
  
  fix: Insert `mvarDeps` Leni Aniva 2024-12-11 00:16:52 -0800
• e0e5c9ec68
  
  chore: Code cleanup Leni Aniva 2024-12-10 23:51:47 -0800
• 755ba13c1b
  
  fix: Set `synthesizeSyntheticMVarsNoPostponing` Leni Aniva 2024-12-10 23:48:46 -0800
• 1d10cd2b20
  
  fix: Collect errored mvars by iterating errorInfo Leni Aniva 2024-12-10 23:16:33 -0800
• 95503c45e4
  
  doc: frontend.process newConstants Leni Aniva 2024-12-10 21:45:57 -0800
• 0725d865de
  
  feat: Print value of arbitrary mvar in goal state Leni Aniva 2024-12-10 12:40:00 -0800
• 681c3fb78d
  
  fix: Disallow indeterminant type `sorry` Leni Aniva 2024-12-10 12:21:56 -0800
• 37a5884be4
  
  fix: Use `ppSyntax` instead of `ppTactic` Leni Aniva 2024-12-09 21:39:33 -0800
• 1527743900
  
  refactor: Optionalize CompilationUnit Leni Aniva 2024-12-09 21:00:33 -0800
• eb0374dfb3
  
  feat: Collect new constants in repl Leni Aniva 2024-12-09 20:57:25 -0800
• 9a69c48cb2
  
  fix: Integration test failure Leni Aniva 2024-12-09 20:42:05 -0800
• dd00d803d1
  
  feat: Collect sorry/elab failure boundaries Leni Aniva 2024-12-09 20:38:27 -0800
• e9cbc6eab3
  
  chore: Update version Leni Aniva 2024-12-09 20:17:55 -0800
• 0b4ded1049
  
  fix: Collect sorrys and type mismatches Leni Aniva 2024-12-09 20:15:53 -0800
• 5ef2b5c118
  
  feat: Collect newly defined constants Leni Aniva 2024-12-09 19:40:00 -0800
• d040d2006c
  
  fix: Do not guard mvar errors in other tactics Leni Aniva 2024-12-09 17:58:08 -0800
• 47d26badc8
  
  feat: Capture mvar errors Leni Aniva 2024-12-09 17:30:33 -0800
• 7fc2bd0d0f
  
  test: Tactic failure on synthesizing placeholder Leni Aniva 2024-12-09 08:15:01 -0800
• 2d068ecd50
  
  fix: Use guarded `isDefEq` Leni Aniva 2024-12-09 00:06:20 -0800
• 17ab2eafd8
  
  fix: Halt on match guard Leni Aniva 2024-12-09 00:03:53 -0800
• ea813e5bc5
  
  feat: Monadic info collection Leni Aniva 2024-12-08 23:21:36 -0800
• b950dc9b1a
  
  fix: Verbose printing of infotree Leni Aniva 2024-12-08 22:51:55 -0800
• 9ede3cf717
  
  feat: InfoTree printing Leni Aniva 2024-12-08 15:38:03 -0800
• 4de53e0547
  
  Merge branch 'dev' into frontend/infotree Leni Aniva 2024-12-08 12:54:19 -0800
• d7457cd386 Merge pull request 'fix: Capture nested tactic failure' (#135) from bug/nested-tactic-failure into dev Leni Aniva 2024-12-07 18:51:25 -0800
• 929311a042
  
  fix: Only signal failure when there is error Leni Aniva 2024-12-06 00:08:20 -0800
• 0415baaaff
  
  chore: Cleanup old `TestM` Leni Aniva 2024-12-05 22:16:20 -0800
• 34a4bf5b73
  
  feat: Export GoalState.tryTactic Leni Aniva 2024-12-05 22:12:04 -0800
• a62ac51c37
  
  chore: Remove all redundant filenames Leni Aniva 2024-12-05 22:11:37 -0800
• 7aafd6956f
  
  fix: Capture composite tactic failure Leni Aniva 2024-12-05 22:07:21 -0800
• 2e2658bde7
  
  test: Add test case for composite tactic Leni Aniva 2024-12-05 21:35:37 -0800
• fb3d36584f
  
  chore: Add formatter, update lean4-nix Leni Aniva 2024-12-05 18:59:14 -0800
• 13dd11e995
  
  chore: Update Lean to v4.14 Leni Aniva 2024-12-05 18:55:30 -0800
• adb44c4fdb Merge pull request 'doc: Design Rationale Document' (#123) from doc/rationale into dev Leni Aniva 2024-12-05 17:24:19 -0800
• 4bd50c17ac
  
  Merge branch 'dev' into doc/rationale Leni Aniva 2024-12-05 17:23:32 -0800
• f59df97c84 Merge pull request 'doc: Documentation cleanup and update' (#133) from chore/cleanup into dev Leni Aniva 2024-12-05 17:23:24 -0800
• 95408d1d52
  
  doc: Unify types Leni Aniva 2024-12-05 17:21:06 -0800
• d00e376943
  
  doc: Remove outdated documentation Leni Aniva 2024-12-05 17:18:35 -0800
• ebf9ab24f7 Merge pull request 'feat: Pickling goal states' (#129) from serial/pickle into dev v0.2.21 Leni Aniva 2024-12-05 16:02:25 -0800
• bfdc7dd39e
  
  doc: Fix code environment Leni Aniva 2024-12-05 16:02:00 -0800
• 3da85b7f04
  
  doc: Documentation for save/load Leni Aniva 2024-12-05 16:00:46 -0800
• c54ce93ef5
  
  feat: Goal State IO in REPL Leni Aniva 2024-12-05 14:31:43 -0800
• 105fb7af4b
  
  feat: Goal state pickling Leni Aniva 2024-12-05 14:23:55 -0800
• 49b0101862 Merge pull request 'feat: Erase macro scopes in sexp' (#130) from delate/sexp into dev Leni Aniva 2024-12-04 11:24:15 -0800
• 0f946880ae
  
  test: Environment pickling Leni Aniva 2024-12-04 10:44:33 -0800
• 7c9b092200
  
  test: Dual monad testing stub Leni Aniva 2024-11-30 23:21:16 -0800
• 44aef76a10
  
  refactor: Remove sanitization for mvarId/fvarId Leni Aniva 2024-11-26 12:57:19 -0800
• a8e7a1a726
  
  feat: Erase macro scopes in sexp Leni Aniva 2024-11-26 12:34:52 -0800
• 9894ad7c7e
  
  refactor: InfoTree functions Leni Aniva 2024-11-26 12:16:14 -0800
• a51bf6f807
  
  Merge branch 'dev' into doc/rationale Leni Aniva 2024-11-17 17:38:27 -0800
• 5d676154f1
  
  doc: Fix documentation link Leni Aniva 2024-11-16 21:27:40 -0800
• ce3af887be
  
  doc: Rationale document Leni Aniva 2024-11-15 23:36:28 -0800
• af256123f3
  
  doc: Update icon Leni Aniva 2024-11-15 23:29:37 -0800
• 1da9180473 Merge pull request 'feat: State and environment pickling' (#120) from serial/pickle into dev Leni Aniva 2024-11-15 23:10:33 -0800
• 4bfd606e2a
  
  Merge branch 'dev' into serial/pickle Leni Aniva 2024-11-15 23:09:08 -0800
• f9d31597ec
  
  chore: Update lean4-nix v0.2.20 Leni Aniva 2024-11-15 14:56:51 -0800
• 6a7ff46fb0 Merge pull request 'chore: Update Lean4 upstream to unofficial flake' (#115) from misc/build into dev Leni Aniva 2024-11-15 14:40:47 -0800
• 0ee7d57570
  
  feat: Expose iTree for LSP Configuration Leni Aniva 2024-11-14 22:51:25 -0800
• 600c27a616
  
  Merge branch 'dev' into misc/build Leni Aniva 2024-11-14 22:44:55 -0800