Commit Graph

Select branches

Hide Pull Requests

dev

doc/rationale

env/inspect

io/async

main

misc/build

parse/level

#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

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

• 4435a6459c Merge pull request 'fix: Use in-context environment in sorry collection' (#166) from bug/collect-sorry-generated-constants into dev 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
• 4123792c0c synced w/ upstream/main (0.2.24) io/async Qi Liu 2025-01-14 11:14:07 +0800
• ac36fd6cd0 added more type hint and options; moved test_server_init_del below test_version Qi Liu 2025-01-14 11:09: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
• 5adbbcae6e
  Merge pull request #57 from lenianiva/version/0.2.24 Leni Aniva 2025-01-10 17:11:21 -0800
• 39aff1da22
  
  chore: Update version flag Leni Aniva 2025-01-10 17:09:47 -0800
• 035dd492d1
  
  fix: Missing flags Leni Aniva 2025-01-10 17:07:35 -0800
• ef4e5ecbf8
  
  chore: Update version v0.2.24 Leni Aniva 2025-01-10 12:55:26 -0800
• e8a15dfc50
  
  chore: Update upstream to candidate Leni Aniva 2025-01-10 12:53:33 -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 env/inspect 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
• f4cc21cc96 Async: implemented; MiniF2F: fixed Qi Liu 2024-12-13 06:15:52 +0000
• 4badb8adab
  Merge pull request #50 from lenianiva/misc/version Leni Aniva 2024-12-11 21:31:06 -0800
• ffacb67a03
  
  fix: DSP output Leni Aniva 2024-12-11 21:30:40 -0800
• 13e01b9e62
  
  Merge branch 'dev' into misc/version Leni Aniva 2024-12-11 20:51:17 -0800
• 2aa5fb2a3d
  
  doc: Update `load_sorry` documentation Leni Aniva 2024-12-11 20:46:39 -0800
• 56fc11f831
  
  fix: Experiments with new `load_sorry` Leni Aniva 2024-12-11 17:32:07 -0800
• ce7e27a0fd
  
  doc: Add doc building instructions Leni Aniva 2024-12-11 17:20:25 -0800
• 04e40b6dfa
  
  doc: Update all examples to 0.2.23 Leni Aniva 2024-12-11 17:14:44 -0800
• 4c559294d3
  
  chore: Update version Leni Aniva 2024-12-11 17:07:50 -0800
• 57001bb0a3
  
  doc: Update documentation Leni Aniva 2024-12-11 17:07:35 -0800
• 8e373eb3b2
  
  fix: Goal state pickling Leni Aniva 2024-12-11 17:00:25 -0800
• f1e3ec82f0
  
  fix: Goal state pickling/unpickling Leni Aniva 2024-12-11 16:54:50 -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
• fb8652d132
  
  feat: Env/Goal pickling Leni Aniva 2024-12-11 16:36:55 -0800
• 359b5f8d47
  
  feat: env.{add, inspect} Leni Aniva 2024-12-11 16:32:12 -0800
• 47b2fbe38d
  
  refactor: Into CompilationUnit objects Leni Aniva 2024-12-11 16:25:45 -0800
• f111da7de7
  
  doc: Add limitations doc/rationale 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
• d3c14f321f
  
  chore: Update to 0.2.22 Leni Aniva 2024-12-11 01:30:52 -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