Commit Graph

Select branches

Hide Pull Requests

bug/variable-level-names-in-scope

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

#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

• 70152c7715
  
  refactor: Optional levels bug/variable-level-names-in-scope 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 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
• 18446f865e Merge pull request 'test: Update LSpec' (#182) from test/build into dev Leni Aniva 2025-03-29 15:44:28 -0700
• 91fbc4cdca
  
  chore: Remove redundant code Leni Aniva 2025-03-29 15:43:49 -0700
• 2885671490
  
  test: Update LSpec Leni Aniva 2025-03-29 15:01:57 -0700
• b9ff9e8f13
  
  feat(repl): Optional type argument in `env.add` Leni Aniva 2025-03-29 14:51:35 -0700
• 9ea099827f
  
  fix(env): Adding declarations with universe levels Leni Aniva 2025-03-29 14:39:42 -0700
• 3c07188cdf Merge pull request 'feat: Tactic with timeout' (#179) from repl/timeout into dev Leni Aniva 2025-03-28 21:31:58 -0700
• 0528a1592e
  
  fix: Print internal exceptions nicely Leni Aniva 2025-03-28 21:31:30 -0700
• 4610348fed
  
  feat: `CoreM` timeout Leni Aniva 2025-03-28 20:42:10 -0700
• be505b8050
  
  feat: Run cancel token with timeout Leni Aniva 2025-03-28 19:06:43 -0700
• 48485a868b Merge pull request 'feat: Update `CoreM` options from parsed header' (#177) from frontend/env-init into dev Leni Aniva 2025-03-28 18:56:21 -0700
• 9980fd9c39
  
  test(repl): Environment loading from header Leni Aniva 2025-03-28 18:45:58 -0700
• 8adab24157
  
  fix: Call sites in `Main.lean` Leni Aniva 2025-03-28 00:56:18 -0700
• c2b7501649
  
  refactor: Remove `CoreM` from `MainM` Leni Aniva 2025-03-28 00:50:39 -0700
• 0fea0b50c9
  
  Merge branch 'dev' into frontend/env-init Leni Aniva 2025-03-25 12:27:32 -0700
• fb91b521fb Merge pull request 'chore: Update Lean to v4.17.0, version to v0.3' (#178) from chore/version into dev Leni Aniva 2025-03-24 18:05:25 -0700
• ebf514b92b
  
  chore: Update nix flake Leni Aniva 2025-03-24 18:04:34 -0700
• d305918bb9
  
  chore: Update Lean to v4.17.0 Leni Aniva 2025-03-24 17:57:34 -0700
• 3e55b4b22f
  
  feat(repl): Record last scope Leni Aniva 2025-03-24 17:47:56 -0700
• bc37482212 Merge pull request 'feat(delate): Unfold matchers' (#176) from delate/instantiate into dev Leni Aniva 2025-03-17 18:37:55 -0700
• cb1082c7c7
  
  chore: More code cleanup Leni Aniva 2025-03-17 12:14:16 -0700
• 678cc9b3c0
  
  chore: Code cleanup Leni Aniva 2025-03-17 11:30:24 -0700
• 4643992c3b
  
  refactor(delate): Unfold matchers into function Leni Aniva 2025-03-17 11:26:13 -0700
• 3b4b196a30
  
  feat(delate): Add mdata annotation for matcher Leni Aniva 2025-03-17 11:20:38 -0700
• a28ad9b239
  
  feat(delate): Expand matcher applications Leni Aniva 2025-03-17 10:47:11 -0700
• dc29d48b77
  
  chore: Remove IO.println for trace Leni Aniva 2025-03-17 09:31:39 -0700
• 78485ae6e2
  
  doc(frontend): Update documentation for `frontend.process` Leni Aniva 2025-03-14 20:07:31 -0700
• 98ad1ae283
  
  feat(delate): Tracing tags Leni Aniva 2025-03-14 16:54:34 -0700
• 8063039f7e Merge pull request 'feat(frontend): Alternative methods of initializing environment' (#173) from frontend/env-init into dev Leni Aniva 2025-03-14 16:48:40 -0700
• ef165b7045
  
  fix(frontend): Test update Leni Aniva 2025-03-14 16:47:46 -0700
• 79e4dc697e
  
  feat(frontend): Add option to inherit environment Leni Aniva 2025-03-14 16:46:28 -0700
• 8797bbe245
  
  test(frontend): Fix the open test Leni Aniva 2025-03-14 16:35:12 -0700
• 896475848b
  
  fix: Name generation not available due to context Leni Aniva 2025-03-10 19:03:14 -0700
• 0cfd73e44e
  
  test(frontend): Add scope `open` test Leni Aniva 2025-03-09 23:29:33 -0700
• 1dceb5428e Merge pull request 'fix: Manifest key error' (#172) from chore/build into dev Leni Aniva 2025-03-08 22:53:07 -0800
• 9e1ea54cbe
  
  chore: Cleanup file filtering system Leni Aniva 2025-03-08 22:52:36 -0800
• 5d0a7e8443
  
  fix: Manifest key error Leni Aniva 2025-03-08 22:50:04 -0800
• 4f5dd97e55 Merge pull request 'chore: Cleanup the library system' (#169) from chore/cleanup into dev Leni Aniva 2025-03-08 21:19:00 -0800
• 7ae50696ac
  
  merge: branch 'dev' into chore/cleanup Leni Aniva 2025-03-08 21:18:45 -0800
• 9cf071eefe
  
  chore: Read manifest for LSpec version Leni Aniva 2025-03-08 21:16:47 -0800
• 92515ea0f2
  
  fix: Update flake lock Leni Aniva 2025-03-08 21:11:59 -0800
• 5a690c4421
  
  chore: Use `fetchGit` for `LSpec` input Leni Aniva 2025-03-08 21:11:34 -0800
• 39ec79e6bb
  
  feat: Monad lifting in `GoalState.withContext` Leni Aniva 2025-03-08 21:07:15 -0800
• 999bb146fa
  
  chore: Remove all unused auxiliary tactics Leni Aniva 2025-03-01 20:12:30 -0800
• 642bca42e9 Merge pull request 'chore: Version bump' (#168) from chore/version into dev Leni Aniva 2025-02-25 15:16:43 -0800
• ec3e1ff2c0
  
  chore: Bump version to 0.3.0-rc.1 Leni Aniva 2025-02-25 15:16:10 -0800
• 76639d0266
  
  fix: Panic edge case for module name Leni Aniva 2025-02-24 15:45:31 -0800
• 267290c8f7
  
  fix: Draft tactic failure by new `sorry` semantics Leni Aniva 2025-02-23 14:14:59 -0800
• aac39ca60c
  
  fix: Some test errors Leni Aniva 2025-02-23 14:13:44 -0800
• 31c76e0d00
  
  chore: Version bump Leni Aniva 2025-02-23 14:10:24 -0800
• 4435a6459c Merge pull request 'fix: Use in-context environment in sorry collection' (#166) from bug/collect-sorry-generated-constants into dev v0.2.25 Leni Aniva 2025-01-28 17:42:54 -0800
• 05f6997062
  
  doc: Update repl documentation Leni Aniva 2025-01-28 17:41:41 -0800
• c77f14d383
  
  fix: Use context environment in sorry capture Leni Aniva 2025-01-28 17:40:49 -0800
• 274e29199d
  
  fix: Use post-step environment in sorry collection Leni Aniva 2025-01-27 19:57:02 -0800
• 4d295bd9ff Merge pull request 'doc: Manual about `env.{describe,module_read}`' (#165) from env/module into dev Leni Aniva 2025-01-26 22:04:28 -0800
• 7d6ad1ebb9 Merge pull request 'chore: Code cleanup' (#164) from chore/cleanup into dev Leni Aniva 2025-01-26 22:04:12 -0800
• 003a63bd13
  
  doc: Manual about `env.{describe,module_read}` Leni Aniva 2025-01-24 20:21:31 -0800
• 970c16a0a4
  
  chore: Use `StateRefT` in `Repl.lean` Leni Aniva 2025-01-24 20:19:07 -0800
• 6a7830cb71
  
  fix: Remove spurious print Leni Aniva 2025-01-24 19:24:54 -0800
• 787c9e606d
  
  chore: Cleanup REPL loop Leni Aniva 2025-01-24 19:22:58 -0800
• 976646fb67
  
  chore: Use repeat-break structure Leni Aniva 2025-01-24 19:11:05 -0800
• 418d630255
  
  fix: Remove unused variable Leni Aniva 2025-01-24 19:06:07 -0800
• b67d3eccc4 Merge pull request 'fix: Panic in `exprProjToApp`' (#161) from bug/expr-proj-to-app-panic into dev Leni Aniva 2025-01-24 15:05:04 -0800
• 6f792b0657
  
  Merge branch 'dev' into bug/expr-proj-to-app-panic Leni Aniva 2025-01-24 15:03:13 -0800
• ed1d5d7b58 Merge pull request 'feat: Module reading functions' (#159) from env/module into dev Leni Aniva 2025-01-24 15:01:16 -0800
• f7f1272145
  
  Merge branch 'dev' into env/module Leni Aniva 2025-01-24 15:01:00 -0800
• be8dee6731
  
  test: Add test for module read Leni Aniva 2025-01-24 15:00:35 -0800
• 549be79cbf Merge pull request 'feat: Pickle constants in goal state' (#157) from serial/pickle into dev Leni Aniva 2025-01-24 14:52:52 -0800
• 5c1e7599c0
  
  feat: Projection export function Leni Aniva 2025-01-24 14:44:09 -0800
• 8ce4cbdcf5
  
  feat: Printing field projection in sexp Leni Aniva 2025-01-22 13:01:47 -0800
• 3a26bb1924
  
  fix: Analyze projection application Leni Aniva 2025-01-22 12:49:33 -0800
• 5994f0ddf0
  
  fix: Conditional handling of `.proj` Leni Aniva 2025-01-17 23:10:03 -0800
• 59935e386b Merge pull request 'feat: Draft tactic REPL interface' (#158) from tactic/draft into dev Leni Aniva 2025-01-16 10:32:47 -0800
• bc4bf47c8b
  
  feat: Implement repl interfaces Leni Aniva 2025-01-15 21:23:37 -0800
• c9f524b9ae
  
  feat: Implement `env.describe` and `env.module_read` Leni Aniva 2025-01-15 21:20:05 -0800
• 4f5ffc1ffb
  
  feat: Protocol for module access Leni Aniva 2025-01-15 21:02:04 -0800
• 62363cb943
  
  fix: Over-eager assertion of fvarId validity Leni Aniva 2025-01-14 13:21:38 -0800
• 9d445783c2
  
  feat: Draft tactic REPL interface Leni Aniva 2025-01-13 12:50:25 -0800
• fef7f1e2f3
  
  feat: Pickle constants in goal state Leni Aniva 2025-01-13 12:43:19 -0800
• c1f63af019 chore: Update version to 0.2.25 Leni Aniva 2025-01-13 10:22:53 -0800
• b8b46c4a9c Merge pull request 'chore: Update Lean to v4.15.0' (#134) from misc/version into dev Leni Aniva 2025-01-13 12:28:49 -0800
• 60e78b322e
  
  fix: Test failures Leni Aniva 2025-01-13 12:28:16 -0800
• 06fdf7e678
  
  chore: Update Lean to v4.15.0 Leni Aniva 2025-01-13 11:09:55 -0800
• 5e61282660
  
  test: Source location extraction Leni Aniva 2025-01-13 10:30:26 -0800
• 9d2a999a4f
  
  merge: branch 'dev' into misc/version Leni Aniva 2025-01-13 10:29:50 -0800
• a3b99279e0
  
  chore: Update version to 0.2.25 Leni Aniva 2025-01-13 10:22:53 -0800
• db24650aec Merge pull request 'feat: Draft tactic' (#153) from goal/tactic-draft into dev Leni Aniva 2025-01-13 10:22:35 -0800
• 6a9ba4bb15
  
  Merge branch 'dev' into goal/tactic-draft Leni Aniva 2025-01-13 10:22:05 -0800
• ebde7c9eed
  
  feat: Prohibit coupling in drafting Leni Aniva 2025-01-13 10:20:36 -0800
• 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