Sebastian Ullrich
1fb1a6f913
fix: do not expose invalid process handles when not redirected
2020-08-30 14:28:56 -07:00
Sebastian Ullrich
cc909e20e1
fix: handle SIGPIPE
2020-08-30 14:28:56 -07:00
Sebastian Ullrich
9f40e46043
feat: basic process API
2020-08-30 14:28:56 -07:00
Sebastian Ullrich
00f176de8d
fix: Windows debug build
2020-08-30 14:28:56 -07:00
Leonardo de Moura
35b11d582d
chore: naming convention
2020-08-30 14:26:03 -07:00
Leonardo de Moura
6f0e9452b2
chore: remove begin ... end syntax
...
We should use `by { ... }` from now on.
cc @Kha
2020-08-30 14:15:33 -07:00
Leonardo de Moura
3a9cfeb9fb
fix: lookahead.formatter
2020-08-30 08:37:51 -07:00
Leonardo de Moura
052e830db7
feat: add have, show, let, let!, and suffices tactic macros
...
They are all simple macros based on: `refine` + syntheticHoles
2020-08-30 08:26:15 -07:00
Leonardo de Moura
0a0ca9f930
fix: funImplicitBinder
2020-08-30 08:10:58 -07:00
Leonardo de Moura
b4f938d859
chore: namedHole => syntheticHole
2020-08-30 08:04:15 -07:00
Leonardo de Moura
89e0fa1488
chore: allow ?_
...
Note that `?_` is not equivalent to `_`. Both do not have a name, but
`?_` is a synthetic metavariable which **cannot** be assigned by typing
constraints, and `_` is a regular metavariable.
We use `?_` to mark an anonymous hole that must be filled using tactics.
@Kha I will rename `namedHole` to `syntheticHole`
2020-08-30 07:54:34 -07:00
Leonardo de Moura
825d9643cd
feat: allow structure instances as fun binder without ()
...
The issue is that `{ x := ... }` was being parsed as an implicit
binder, and we were getting an error at `:=`.
2020-08-30 07:35:41 -07:00
Leonardo de Moura
fc65b76331
feat: lift useful binder term syntax to tactics
2020-08-30 07:15:42 -07:00
Leonardo de Moura
2eb330e36a
feat: improve clear tactic
2020-08-29 20:19:33 -07:00
Leonardo de Moura
9e075e39a5
feat: eval new intro "macro"
...
It is as powerful as the new `fun` term
2020-08-29 17:09:21 -07:00
Leonardo de Moura
3d3238c7fe
fix: typo at introNCoreAux
2020-08-29 17:00:59 -07:00
Leonardo de Moura
52c86e918d
fix: match
2020-08-29 16:38:50 -07:00
Leonardo de Moura
a9e70a4d83
feat: intro similar to fun
2020-08-29 15:15:24 -07:00
Leonardo de Moura
af86cc801d
feat: add change tactic parser
2020-08-29 08:10:55 -07:00
Leonardo de Moura
0288ed0129
feat: add change and changeHypothesis
2020-08-29 08:10:55 -07:00
Leonardo de Moura
70827cb9af
chore: add throwIllFormedSyntax
2020-08-29 08:10:55 -07:00
Leonardo de Moura
e5c35d3a4e
feat: add AddMessageDataContext
2020-08-28 18:05:42 -07:00
Leonardo de Moura
99f3296828
refactor: simplify Util/Trace.lean
2020-08-28 17:36:44 -07:00
Leonardo de Moura
26073c428b
fix: use MonadFinally
2020-08-28 17:06:40 -07:00
Leonardo de Moura
39d456cb09
feat: add polymorphic trace and logTrace
...
This commit also makes sure we always use `withContext` when logging.
2020-08-28 16:49:24 -07:00
Leonardo de Moura
5e582823ec
feat: add MonadLCtx and MonadMCtx helper classes
2020-08-28 16:48:42 -07:00
Leonardo de Moura
65f1c3fe65
chore: simplify MonadMacroAdapter
2020-08-28 16:24:06 -07:00
Leonardo de Moura
e0d39e6a7d
feat: use whnf at subst
2020-08-28 15:56:28 -07:00
Leonardo de Moura
cc47705691
chore: remove import Init.*
2020-08-28 15:39:08 -07:00
Leonardo de Moura
64840c10c3
chore: cleanup Log.lean
2020-08-28 15:26:35 -07:00
Leonardo de Moura
212fd22594
chore: remove dead fields
2020-08-28 15:04:24 -07:00
Leonardo de Moura
2287c7e7b3
feat: elaborate #print axioms command
2020-08-28 13:08:42 -07:00
Leonardo de Moura
cc1c9f3dfb
feat: add #print axioms
2020-08-28 12:26:07 -07:00
Leonardo de Moura
27170cddb9
feat: mark Lean.ofReduceBool and Lean.ofReduceNat as axioms
...
The idea is to inform users whether their trust code base depends on
the compiler, interpreter, `[implementedBy]` and `[extern]`
annotations.
2020-08-28 12:22:12 -07:00
Sebastian Ullrich
95901a0346
fix: make Stream.ofBuffer thread-safe
2020-08-28 10:04:32 -07:00
Sebastian Ullrich
110ae4b571
feat: replace OS-specific stream redirection with pure-Lean Stream redirection
...
This avoids the temporary files workaround on macOS and Windows, and makes sure
we can process a `#eval` command and write messages to stdout at the same time.
2020-08-28 10:04:32 -07:00
Sebastian Ullrich
efa119bc94
feat: make std streams Streams
2020-08-28 10:04:32 -07:00
Sebastian Ullrich
56fda835be
feat: add ByteArray <-> String conversions
2020-08-28 10:04:32 -07:00
Sebastian Ullrich
dbebff3a2d
feat: ByteArray.copySlice
2020-08-28 10:04:32 -07:00
Sebastian Ullrich
1b0ffbb74d
feat: make std IO streams settable
...
Co-authored-by: Simon Hudon <simon.hudon@gmail.com>
2020-08-28 10:04:32 -07:00
Leonardo de Moura
091000462d
chore: remove unnecessary node
2020-08-28 09:43:23 -07:00
Leonardo de Moura
62177069fd
fix: induction tactic
2020-08-28 09:18:22 -07:00
Leonardo de Moura
4bc1be17f4
chore: cleanup
2020-08-28 09:18:22 -07:00
Sebastian Ullrich
479f001de4
chore: reduce Parser <- Elab dependencies
2020-08-28 12:39:12 +02:00
Leonardo de Moura
0b7a7f7b90
feat: better support for _ in match tactic
2020-08-27 18:18:49 -07:00
Leonardo de Moura
76bda91ff8
feat: add evalMatch for tactics
2020-08-27 18:05:06 -07:00
Leonardo de Moura
2914388f19
fix: mkTacticMVar
...
Incorrect `Syntax` being used to report error messages.
2020-08-27 16:42:47 -07:00
Leonardo de Moura
7a62b290f7
fix: use getMVarsNoDelayed in tactics
2020-08-27 16:28:15 -07:00
Leonardo de Moura
d2f9f250db
feat: add match tactic parser
2020-08-27 15:57:05 -07:00
Leonardo de Moura
7a6effa54f
chore: cleanup
2020-08-27 15:47:58 -07:00
