max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
26426 commits 1 branch 0 tags 5.3 GiB
Commit graph

142 commits

Author SHA1 Message Date
tydeu
7fcfb78fd5 feat: use BaseIO at MonadLift (ST IO.RealWorld) 2021-11-09 09:11:33 +01:00
Leonardo de Moura
7e0bc23e5d chore: cleanup syntax 2021-11-05 15:03:57 -07:00
Mac
eb5852448e
feat: generalize IO task functions to BaseIO := EIO Empty (#744) 
* feat: generalize `asTask`/`bindTask`/`mapTask` to `EIO`

* feat: generalize task functions to the `EIO Empty` monad

* chore: fix test + correct doc

* feat: further generalize task functions to `RealM := EIO Empty`

* chore: `RealM`/Task API touch-ups

* refactor: `abbrev RealM` -> `def BaseIO`

* chore: remame args / remove `EIO.toBaseIO_` as per code review

* refactor: use `BaseIO` at `checkCanceled`/`getNumHeartbeats`

* chore: fix `lean_io_bind_task_fn` signature error
 2021-11-04 15:37:55 -07:00
Sebastian Ullrich
08c2c31fcd feat: IO.FS.removeDir(All) 2021-09-16 07:01:37 -07:00
Leonardo de Moura
218b9c87b0 feat: expose APIs for creating IO.Error objects 2021-09-11 17:14:43 -07:00
Leonardo de Moura
3714cf16ec refactor: lazy evaluation for <|> 
see #617
 2021-09-07 17:06:10 -07:00
Leonardo de Moura
a821dcbff2 chore: enforce naming convention for theorems 
see issue #402

fix: `ElabTerm.lean`
 2021-08-07 12:48:38 -07:00
Leonardo de Moura
b986bde639 fix: IO.Error.alreadyExists may have an optional file name 
We got an assertion violation yesterday at `leanpkg` at
```cpp
  case EEXIST: case EINPROGRESS: case EISCONN:
        lean_assert(fname == nullptr);   // <<<<<<< HERE
        return lean_mk_io_error_already_exists(errnum, details);
```
 2021-07-27 07:00:06 -07:00
Wojciech Nawrocki
f27a069773 chore: drop UntypedRef and use monotonic RpcRefs 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
b3d9e90695 feat: IO.getRandomBytes 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
85dcdcde93 chore: use NonScalar 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
2e6382e1c7 feat: untyped references 2021-07-24 10:45:28 +02:00
Sebastian Ullrich
2091a09fa1 feat: IO.Process.Child.takeStdin 2021-06-11 17:53:51 -07:00
Daniel Selsam
a22bba7bbf feat: Process.exit 
Closes #356
 2021-06-11 17:53:51 -07:00
Sebastian Ullrich
1ebcf76d48 refactor: remove explicitly lifted IO functions and move more things into IO.FS 
Automatic lifting takes care of this, and it wasn't consistently applied anyway
 2021-06-11 17:53:51 -07:00
Wojciech Nawrocki
485f8ea2d0 feat: setup Emscripten file paths 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
8ada0ba043 feat: initial Emscripten support 2021-06-06 15:34:44 +02:00
Sebastian Ullrich
3fb7a2c0e1 fix: make problematic Ord -> LT instance a def 2021-05-31 19:05:50 -07:00
Sebastian Ullrich
6857076df4 feat: leanpkg build without external dependencies 2021-05-30 17:29:54 +02:00
Sebastian Ullrich
a9fa84815b feat: IO.createDir, IO.createDirAll 2021-05-30 17:29:54 +02:00
Sebastian Ullrich
94aea76922 feat: FilePath.metadata 2021-05-30 17:29:54 +02:00
Sebastian Ullrich
e4995ce8ba feat: add convenience coercion from String to FilePath 2021-05-28 14:19:59 +02:00
Sebastian Ullrich
619873c842 feat: make System.FilePath opaque 2021-05-28 14:19:59 +02:00
Sebastian Ullrich
4354534fda feat: make FilePath a concrete type 
Resolves #363
 2021-05-28 14:19:59 +02:00
Sebastian Ullrich
2988897cac feat: IO.FS.readDir 2021-05-26 09:47:43 +02:00
Leonardo de Moura
b85c60aa75 chore: remove leftovers 2021-03-23 17:33:23 -07:00
Sebastian Ullrich
ed55fdfd3e chore: better error message when failing to find current package 2021-03-23 12:10:26 +01:00
Leonardo de Moura
1112ab6eff chore: use new notation 2021-03-11 11:19:33 -08:00
Wojciech Nawrocki
28d6a1ebe1 fix: go-to-def paths on Windows 2021-01-28 11:45:33 -08:00
Leonardo de Moura
acfac85ac0 feat: add IO.getNumHeartbeats 2021-01-24 17:45:50 -08:00
Wojciech Nawrocki
a3f5aca22f fix: tail-recursive readBinToEnd 2021-01-22 18:02:31 +01:00
Wojciech Nawrocki
8addea6e74 chore: remove Handle.size 2021-01-22 18:02:31 +01:00
Sebastian Ullrich
0c91b3769e chore: replace variables in src/ 2021-01-22 14:36:05 +01:00
Sebastian Ullrich
e662992533 feat: IO.removeFile 2021-01-19 19:06:01 +01:00
Leonardo de Moura
bfc1a16c02 chore: adjust instance param order 2021-01-13 18:31:41 -08:00
Sebastian Ullrich
4a262fbc5b fix: remove auto-cancellation of IO tasks 
Chained tasks were never auto-canceled, so let's be explicit everywhere
 2020-12-30 17:03:09 +01:00
Sebastian Ullrich
4a22854b1e chore: make server tests fixable 2020-12-27 15:05:29 +01:00
Wojciech Nawrocki
3fca58ea8c feat: IO.FS.Handle.size 2020-12-23 20:00:36 +01:00
Sebastian Ullrich
3cdcdac921 feat: infer worker path 2020-12-23 20:00:36 +01:00
Marc Huisinga
088c3347cd feat: adjust file worker for new IO features 2020-12-23 20:00:36 +01:00
Leonardo de Moura
d4ae9e73b1 fix: missing comma 2020-12-15 20:29:28 -08:00
Leonardo de Moura
3b6d65c3c3 chore: use deriving Inhabited 2020-12-13 10:09:20 -08:00
Leonardo de Moura
91dec25a35 fix: bug at runST and runEST 2020-12-06 18:52:28 -08:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
d6f778bec4 refactor: arbitrary without explicit arguments 
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
 2020-11-25 09:07:38 -08:00
Leonardo de Moura
495b6a92e9 feat: add IO.sleep ms 
I am going to use it in the documentation: `Task` examples.
 2020-11-24 11:27:04 -08:00
Leonardo de Moura
be812081f4 chore: using "unbound implicit locals" 2020-11-23 13:09:02 -08:00
Leonardo de Moura
cb9574b086 chore: test unboundImplicitLocals and cleanup 2020-11-22 10:33:28 -08:00
Leonardo de Moura
90298ba476 feat: add helper instance 2020-11-19 11:32:54 -08:00
Leonardo de Moura
304c80d610 feat: use <| 2020-11-19 09:03:38 -08:00