tydeu
99b78bcc23
fix: stdin := .null in IO.Process.output
2023-10-12 08:55:26 +02:00
int-y1
ce4ae37c19
chore: fix more typos in comments
2023-10-08 14:37:34 -07:00
Joachim Breitner
6b429fed8f
doc: fix markup in IO.RealWorld ( #2430 )
...
so that
<https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#IO.RealWorld >
looks good.
2023-08-17 11:55:03 -07:00
tydeu
736af918f5
doc: IO.Process.getPID tweak + IO.FS.Mode
2023-08-14 18:42:04 +02:00
tydeu
c79c7c89b3
feat: IO.Process.getPID & IO.FS.Mode.writeNew
2023-08-08 16:23:43 -04:00
Mario Carneiro
dd313c6894
feat: add IO.FS.rename
2023-07-22 23:21:32 +02:00
Sebastian Ullrich
9901804a49
feat: SpawnArgs.setsid, Child.kill
2023-07-05 23:42:53 +02:00
Sebastian Ullrich
a4f732e6b1
fix: ignore vanishing files during watchdog update
2023-03-10 19:13:24 +01:00
Sebastian Ullrich
113de7cca1
refactor: move from fopen to open
2023-03-10 16:27:56 +01:00
Sebastian Ullrich
aacab14394
chore: remove support for text-mode I/O
...
This didn't do anything except on Windows, where it would make the
application differ from standard Windows applications, which we don't
want.
2023-03-10 16:27:56 +01:00
Leonardo de Moura
0739c9ccd7
chore: revert workaround
2023-01-04 09:02:02 -08:00
Gabriel Ebner
cb7657f47e
fix: remove nonempty_list tactic
2023-01-03 18:17:19 -08:00
Gabriel Ebner
a2f5959118
chore: use deriving Nonempty
2022-12-22 03:48:15 +01:00
Gabriel Ebner
14f8ff1642
feat: add CoeOut class
2022-12-21 04:24:39 +01:00
Gabriel Ebner
c7fb3a1c91
chore: make use of CoeHead chaining
2022-12-21 04:24:39 +01:00
Henrik Böving
24cc6eae6d
feat: log2 for Fin and UInts
2022-11-29 01:05:06 +01:00
E.W.Ayers
691835037e
feat: code action resolvers
2022-10-20 11:20:42 -07:00
Mario Carneiro
583e023314
chore: snake-case attributes (part 2)
2022-10-19 09:28:08 -07:00
Gabriel Ebner
0c2a5580cb
feat: enforce correct syntax kind in macros
2022-10-18 14:59:14 -07:00
Leonardo de Moura
870de844dc
chore: annotate relevant monadic code with [alwaysInline]
...
TODO: after we delete old code generator, we should replace
`@[alwaysInline, inline]` with `@[alwaysInline]`.
Remainder: we want the old code generator to ignore `@[alwaysInline]`
annotations, in particular, the new ones on `instance` commands that
are actually annotations for the instance methods.
2022-10-12 19:48:02 -07:00
Sebastian Ullrich
48d3bbdde9
fix: explicit drive letter normalization in FilePath <-> URI conversions
2022-10-08 10:12:11 -07:00
Sebastian Ullrich
8d34cc15cf
fix: path normalization should not case-normalize entire path
2022-10-08 10:12:11 -07:00
Leonardo de Moura
04b32eb140
chore: remove noinline and nospecialize from runEval
2022-09-07 13:08:01 -07:00
Gabriel Ebner
7c552380da
feat: Mutex, Condvar
2022-09-05 08:52:46 -07:00
Gabriel Ebner
c2f1e01b3b
feat: Promise
2022-09-05 08:52:46 -07:00
Gabriel Ebner
451f6df5df
fix: IO.waitAny requires nonempty list
2022-09-05 08:52:46 -07:00
Gabriel Ebner
20f41deea7
feat: add Eval instance for BaseIO
2022-09-05 08:52:46 -07:00
Gabriel Ebner
22c3ec3996
chore: generalize IO.sleep to BaseIO
2022-09-05 08:52:46 -07:00
Mario Carneiro
850ee17346
chore: move Bootstrap.System.Uri to Init
2022-08-29 08:06:30 -07:00
Sebastian Ullrich
12d7e839b0
doc: Stream.read/getLine
2022-08-26 20:55:09 -07:00
Sebastian Ullrich
a69d7fb018
fix: remove broken Handle.isEof
2022-08-26 20:55:09 -07:00
Sebastian Ullrich
d23c19884b
doc: read/getLine EOF behavior
2022-08-26 20:55:09 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Leonardo de Moura
fc7c1d1053
chore: remove unnecessary set_option
2022-06-28 17:37:10 -07:00
Sebastian Ullrich
d9cfda4893
refactor: make more use of quotations
...
Automatically fixes many TSyntax type errors
2022-06-27 22:37:02 +02:00
Leonardo de Moura
f6d1e48cb8
fix: constant => opaque issues
2022-06-14 17:19:54 -07:00
Leonardo de Moura
02c4e548df
feat: replace constant with opaque
2022-06-14 17:02:59 -07:00
Leonardo de Moura
041827bed5
chore: unused variables
2022-06-07 17:54:10 -07:00
Sebastian Ullrich
897a5de6ac
chore: revert some questionable signature changes
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Leonardo de Moura
305d8e641c
chore: style
2022-04-23 10:47:53 -07:00
Sebastian Ullrich
b6446902c2
feat: server.stderrAsMessages option
...
/cc @leodemoura
2022-04-19 22:29:26 +02:00
Jannis Limperg
5ff8f64255
feat: add IO.monoNanosNow
2022-04-11 12:16:20 +02:00
Leonardo de Moura
3862e7867b
refactor: make String.Pos opaque
...
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`
closes #410
2022-03-20 10:47:13 -07:00
Joscha
841d51a7e6
fix: walkDir
2022-02-05 19:55:09 +01:00
Leonardo de Moura
12e2a79170
chore: fix codebase after removing auto pure
2022-02-03 18:08:14 -08:00
Leonardo de Moura
bac91b9b5b
chore: remove arbitrary
2022-01-15 12:14:27 -08:00
Leonardo de Moura
b0d9c16c7a
chore: rename PointedType => NonemptyType
2022-01-15 11:43:53 -08:00
Leonardo de Moura
e3241e82bc
feat: define PointedType as { α : Type u // Nonempty α }
2022-01-14 20:36:51 -08:00
Sebastian Ullrich
6ec406b7d0
feat: System.FilePath.walkDir
2022-01-14 16:22:14 +01:00
