Pantograph

Commit Graph

Select branches

Hide Pull Requests

bug/expr-proj-to-app-panic

dev

doc/rationale

env/inspect

env/module

io/async

main

misc/build

parse/level

serial/pickle

#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

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

v0.2.6

v0.2.7

v0.2.8

v0.2.9

5994f0ddf0

fix: Conditional handling of `.proj` bug/expr-proj-to-app-panic Leni Aniva 2025-01-17 23:10:03 -0800
59935e386b Merge pull request 'feat: Draft tactic REPL interface' (#158) from tactic/draft into dev dev Leni Aniva 2025-01-16 10:32:47 -0800
bc4bf47c8b

feat: Implement repl interfaces env/module 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 serial/pickle 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
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
309975657a

Merge pull request #49 from lenianiva/bug/wheel Leni Aniva 2024-12-10 17:27:21 -0800
1aacbfa42e

doc: Add documentation about using wheel Leni Aniva 2024-12-10 16:40:07 -0800
b5a711202c

fix: Force poetry to include executable in wheel Leni Aniva 2024-12-10 16:36:41 -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