Commit Graph

Select branches

Hide Pull Requests

dev

frontend/tomogram

main

repl/test

serial/delta

#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

#187

#189

#193

#194

#195

#199

#2

#20

#200

#201

#202

#205

#207

#208

#209

#21

#211

#212

#214

#215

#216

#217

#218

#219

#220

#221

#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

v0.3.0

v0.3.1

v0.3.2

Mono Color

• 349cff6f05
  
  test(goal): Collision of aux lemma names serial/delta Leni Aniva 2025-06-26 16:41:49 -0700
• f914e161e8
  
  fix(goal): Reset messages in replay Leni Aniva 2025-06-26 16:23:10 -0700
• 4df8fcda97
  
  Merge branch 'dev' into serial/delta Leni Aniva 2025-06-26 15:52:36 -0700
• 7c300e081d Merge pull request 'feat(goal): Add unshielded tactic execution mode' (#219) from goal/automatic-mode into dev dev Leni Aniva 2025-06-26 15:52:16 -0700
• 52f71f035e
  
  feat(serial): Background environment in pickling Leni Aniva 2025-06-26 15:51:42 -0700
• 9a9659fdb2
  
  feat(delate): Show fragments for each goal Leni Aniva 2025-06-26 14:22:51 -0700
• 1de8df73f8
  
  refactor(goal): Delete unused functions Leni Aniva 2025-06-26 14:08:22 -0700
• 4d9e229707
  
  refactor(repl): Tactic into goal section Leni Aniva 2025-06-26 12:11:27 -0700
• 7fba24d57a
  
  fix(tactic): Filter out sibling fragments Leni Aniva 2025-06-26 11:48:28 -0700
• 425825bf20
  
  test: Fragment cleanup Leni Aniva 2025-06-26 11:45:15 -0700
• 4b02d73374
  
  fix: Tactic fragments inline with C/R paradigm Leni Aniva 2025-06-26 11:37:14 -0700
• ed5854841b
  
  fix: Allow conv tactics to emit non-conv goals Leni Aniva 2025-06-26 10:32:38 -0700
• 25820aa188
  
  test: Move fragment tests to their own file Leni Aniva 2025-06-26 09:52:01 -0700
• 86f2e64939
  
  feat(repl): Use site to handle automatic mode Leni Aniva 2025-06-25 16:27:04 -0700
• 42bb20df4a
  
  refactor(goal): Use site in goal state functions Leni Aniva 2025-06-25 14:35:38 -0700
• 0b731273b2
  
  refactor(goal): A state can have multiple parents Leni Aniva 2025-06-25 13:07:47 -0700
• 53ea808c90
  
  feat(frontend): Dissect syntax tree frontend/tomogram Leni Aniva 2025-06-24 15:31:46 -0700
• 1a9e450066
  
  refactor: Rename `tomogram` to `tomograph` Leni Aniva 2025-06-24 15:23:59 -0700
• d7001c1b28
  
  chore: Tomogram stub Leni Aniva 2025-06-24 15:11:51 -0700
• 8e35926b5c
  
  feat(goal): Tactic action site Leni Aniva 2025-06-24 15:05:24 -0700
• 3e266dc505 Merge pull request 'feat(goal): Branch unification' (#217) from goal/branch-unification into dev Leni Aniva 2025-06-24 13:56:14 -0700
• 9eb5533166
  
  Merge branch 'dev' into goal/branch-unification Leni Aniva 2025-06-24 13:55:34 -0700
• 7837ddff4f
  
  feat(goal): Unify fragments in replay Leni Aniva 2025-06-24 13:51:33 -0700
• 8982cb13a9 Merge pull request 'feat(serial): Robust environment extension pickling' (#216) from serial/env-extensions into dev Leni Aniva 2025-06-24 13:41:05 -0700
• 9b0d96f422
  
  feat(goal): Trace messages for replay Leni Aniva 2025-06-24 13:37:49 -0700
• 9d4b1ae755
  
  refactor(goal): Allow multiple fragments Leni Aniva 2025-06-24 13:31:55 -0700
• 58ae791da3
  
  refactor: `conv` and `calc` into tactic fragments Leni Aniva 2025-06-23 20:57:53 -0700
• 05a8e3b13c
  
  feat: Branch unification (modulo conv/calc) Leni Aniva 2025-06-23 13:09:08 -0700
• cb7c4d2723
  
  chore: Add `_m` suffix to replay Leni Aniva 2025-06-20 17:26:04 -0700
• 343ecc2659
  
  feat(goal): GoalState.replay stub Leni Aniva 2025-06-20 17:25:23 -0700
• cd8c08fe38 Merge pull request 'chore: Update Nix flake' (#214) from chore/toolchain into dev Leni Aniva 2025-06-20 14:03:06 -0700
• 9304cf2368
  
  chore: Update version to 0.3.3 Leni Aniva 2025-06-20 12:29:00 -0700
• 6323c02f47
  
  test: Fix pickle state name Leni Aniva 2025-06-20 12:25:40 -0700
• dfa491a5c2
  
  test: Pickling of aux lemma Leni Aniva 2025-06-20 12:10:31 -0700
• 9d9f5dee88
  
  test: Use synthetic tactic to generate aux lemmas Leni Aniva 2025-06-20 12:00:25 -0700
• b3f88f5d54
  
  Merge branch 'dev' into serial/env-extensions Leni Aniva 2025-06-20 10:50:29 -0700
• 0db2451c8a Merge pull request 'fix: Use the correct unfold aux lemma' (#215) from bug/unfold-aux-lemma into dev Leni Aniva 2025-06-20 10:21:00 -0700
• 771f8ad266
  
  chore: Formatting Leni Aniva 2025-06-20 10:20:33 -0700
• 1b2a2d5c8d
  
  test: Intentionally generate aux lemmas Leni Aniva 2025-06-20 10:19:42 -0700
• 7d9d3e4742
  
  fix: Use the correct unfold aux lemma Leni Aniva 2025-06-19 15:47:16 -0700
• d1d6493d09
  
  chore: Update Nix flake Leni Aniva 2025-06-19 14:50:49 -0700
• 9a8b5040f5 Merge pull request 'chore: Update Lean to v4.20.1' (#209) from chore/toolchain into dev v0.3.2 Leni Aniva 2025-06-18 16:39:18 -0700
• 66eb98397b
  
  merge: branch 'dev' into chore/toolchain Leni Aniva 2025-06-18 15:10:21 -0700
• 9645f706d4
  
  chore: Update lean4-nix Leni Aniva 2025-06-18 14:38:56 -0700
• b7f0ae435a
  
  test: Use `withTempFile` to ensure graceful exit Leni Aniva 2025-06-18 14:35:22 -0700
• 8fd3649f32 Merge pull request 'chore: Update version to 0.3.2' (#212) from chore/version into dev Leni Aniva 2025-06-18 14:28:34 -0700
• 04cbc55f3a
  
  doc: Update invocations usage Leni Aniva 2025-06-17 11:56:31 -0700
• 292fb0be4b
  
  chore: Update version to 0.3.2 Leni Aniva 2025-06-17 11:54:38 -0700
• 86f69dd08c Merge pull request 'refactor: Use syntax tactic in unit test' (#207) from goal/tactic into dev Leni Aniva 2025-06-17 11:51:35 -0700
• ba84456f89 Merge pull request 'feat: Output tactic invocation data to file' (#208) from frontend/tactic-invocation into dev repl/test Leni Aniva 2025-06-17 11:42:36 -0700
• a8b7f69632
  
  fix(env): Use documentUriFromModule Leni Aniva 2025-06-17 11:10:52 -0700
• b2b7cc388a
  
  chore: Fix most test failures Leni Aniva 2025-06-17 10:54:10 -0700
• 3ce335ebfe
  
  chore: Update Lean to v4.20.1 Leni Aniva 2025-06-17 08:38:03 -0700
• 22716597d3
  
  feat(frontend): Write invocation points to file Leni Aniva 2025-06-16 18:10:11 -0700
• 0bdb41635b
  
  refactor: Use syntax tactic in unit test Leni Aniva 2025-06-16 14:05:05 -0700
• 3d65f6a69e Merge pull request 'chore: Code cleanup' (#202) from chore/cleanup into dev Leni Aniva 2025-06-16 13:57:26 -0700
• b7c9867217
  
  Merge branch 'dev' into chore/cleanup Leni Aniva 2025-06-16 13:55:53 -0700
• 975a6f525c Merge pull request 'chore: Update Lean to v4.19.0' (#205) from chore/toolchain into dev Leni Aniva 2025-06-16 13:54:08 -0700
• 0fa5ac335e
  
  fix: Load environment extensions Leni Aniva 2025-06-16 13:45:57 -0700
• d41ec67a63
  
  chore: Update Lean to v4.19.0 Leni Aniva 2025-05-07 09:53:29 -0400
• eb41c179d1
  
  feat(repl): Conditional environment inheritance Leni Aniva 2025-05-02 11:40:32 -0400
• 4bb44dd56a
  
  chore: Syntax cleanup in repl Leni Aniva 2025-05-02 11:33:11 -0400
• 3bb8e75787
  
  chore: Code cleanup Leni Aniva 2025-05-02 11:26:17 -0400
• 120eb90291 Merge pull request 'chore: Update version' (#195) from chore/version into dev v0.3.1 Leni Aniva 2025-05-01 10:41:47 -0700
• 7578e9e180 Merge pull request 'doc: Add design limitations about memory' (#200) from doc/rationale into dev Leni Aniva 2025-05-01 10:40:52 -0700
• df370b0bff
  
  Merge branch 'dev' into chore/version Leni Aniva 2025-05-01 13:39:28 -0400
• 7b9361c72b Merge pull request 'feat(goal): Detect unsafe and sorry' (#201) from goal/detect-unsafe-sorry into dev Leni Aniva 2025-05-01 10:37:59 -0700
• ad55ea1a27
  
  feat(repl): Detection of sorrys Leni Aniva 2025-05-01 13:37:35 -0400
• 8c1cea17e3
  
  fix(goal): Over-eager deduplication of goals Leni Aniva 2025-05-01 13:34:27 -0400
• 4db09c3abc
  
  feat(goal): Check unsafe and sorry Leni Aniva 2025-05-01 13:05:04 -0400
• beef22b945
  
  doc: Add design limitations about memory Leni Aniva 2025-05-01 12:30:17 -0400
• 06071c1044 Merge pull request 'fix: Shield tactics from the environment generated by `frontend.process`' (#199) from bug/exact-question-mark into dev Leni Aniva 2025-05-01 09:26:53 -0700
• f214496c8f
  
  Merge branch 'dev' into bug/exact-question-mark Leni Aniva 2025-05-01 12:25:08 -0400
• b039018578
  
  Merge branch 'main' into bug/exact-question-mark Leni Aniva 2025-05-01 12:24:50 -0400
• 49d06e8c05
  
  fix: Shield tactics from newly created environment Leni Aniva 2025-05-01 12:21:32 -0400
• 0a987174bc Merge pull request 'fix(repl): Elaborate with `errToSorry` as false by default' (#187) from repl/elab-option into dev Leni Aniva 2025-05-01 09:00:02 -0700
• eca7431977 Merge pull request 'fix(goal): Prevent duplication in idempotent tactics' (#193) from bug/resume-goal-duplication into dev Leni Aniva 2025-05-01 08:59:36 -0700
• 170099525c
  
  test: Add tactic edge cases test Leni Aniva 2025-05-01 11:09:43 -0400
• 3653465ded
  
  chore: Update version Leni Aniva 2025-04-20 09:34:28 -0700
• a2f9d77cb5 Merge pull request 'feat(repl): Flush stdout' (#194) from repl/flush into dev Leni Aniva 2025-04-20 09:29:03 -0700
• a88829f9be
  
  Merge branch 'dev' into repl/flush Leni Aniva 2025-04-20 09:28:54 -0700
• d9c484230b
  
  feat(repl): Flush stdout Leni Aniva 2025-04-20 09:19:51 -0700
• fa5d423005 Merge pull request 'doc: Update rationale' (#189) from doc/rationale into dev Leni Aniva 2025-04-18 01:08:23 -0700
• c68fed6657
  
  fix(goal): Use `immediateResume` to handle goal Leni Aniva 2025-04-18 00:38:54 -0700
• 60f79f5f02
  
  doc: Fix typo Leni Aniva 2025-04-14 23:26:14 -0700
• 4abe2fa72f
  
  fix: LEAN_PATH example Leni Aniva 2025-04-14 16:27:29 -0700
• 77b517f4c6
  
  doc: Update rationale about timeout Leni Aniva 2025-04-13 22:55:41 -0700
• 14b74b612d
  
  fix(repl): Elaborate with `errToSorry` as false by default Leni Aniva 2025-04-10 23:13:35 -0700
• 4e44b147e0 Merge pull request 'chore: Version 0.3' (#136) from dev into main v0.3.0 main Leni Aniva 2025-04-09 00:23:18 -0700
• c547d9c8dc Merge pull request 'chore: Update Lean to v4.18.0' (#185) from chore/version into dev Leni Aniva 2025-04-08 10:59:53 -0700
• 13b03b602b
  
  chore: Update flake Leni Aniva 2025-04-08 10:59:37 -0700
• b6c3f7d8fd
  
  chore: Update Lean to v4.18.0 Leni Aniva 2025-04-08 10:54:23 -0700
• 27a1f420ba Merge pull request 'fix: `variable` and `universe` commands in environment capture' (#183) from bug/variable-level-names-in-scope into dev Leni Aniva 2025-04-07 20:18:49 -0700
• 5df3d2bee1
  
  refactor: Remove `runTermElabM` from library Leni Aniva 2025-04-07 20:17:58 -0700
• 9216e4fa86
  
  chore: Format code Leni Aniva 2025-04-07 11:51:48 -0700
• f42af9f6a8
  
  fix: Level name capture Leni Aniva 2025-04-05 14:26:22 -0700
• 70152c7715
  
  refactor: Optional levels Leni Aniva 2025-04-03 14:38:40 -0700
• cf4a5955e3
  
  test: Non-matchers are not matchers Leni Aniva 2025-04-03 11:18:17 -0700
• 1402a69eea Merge pull request 'fix: `env.add` Declarations with universe levels' (#181) from bug/env-add-level into dev Leni Aniva 2025-03-29 15:48:12 -0700
• 664516f148
  
  Merge branch 'dev' into bug/env-add-level Leni Aniva 2025-03-29 15:44:53 -0700