Assorted IO improvements #519
Conversation
| @@ -445,6 +445,8 @@ def run (args : SpawnArgs) : IO String := do | |||
| throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode | |||
| pure out.stdout | |||
|
|
|||
| @[extern "lean_io_exit"] constant exit : UInt8 → IO α | |||
There was a problem hiding this comment.
I moved it into Process following Rust
src/Init/System/IO.lean
Outdated
|
|
||
| def withStdin [MonadFinally m] (h : FS.Stream) (x : m α) : m α := do | ||
| def withStdin [MonadFinally IO] (h : FS.Stream) (x : IO α) : IO α := do |
There was a problem hiding this comment.
The [MonadFinally IO] argument seems unnecessary now. withStdin also seems more useful in the m α → m α version.
src/Init/System/IO.lean
Outdated
| let mode := | ||
| match m with | ||
| match IO with |
…into `IO.FS` Automatic lifting takes care of this, and it wasn't consistently applied anyway
The names were taken from `llvm-config`
|
Since you added |
|
Also, would this be a good time to make |
I believe that could negatively influence the generated code. edit: rather, see most recent change of that line |
|
Ah, thanks! That explains it. I am surprised, though, that unsafe code can't see through a defined |
|
|
||
| @[inline] | ||
| def withFile (fn : FilePath) (mode : Mode) (f : Handle → m α) : m α := | ||
| def withFile (fn : FilePath) (mode : Mode) (f : Handle → IO α) : IO α := |
There was a problem hiding this comment.
What is the reasoning for applying this change to functions that take monadic callbacks? I often used withFile with an f that does not return IO. What is the recommended workaround?
There was a problem hiding this comment.
I thought I had reverted all higher-order uses of m, but apparently not. Will revert as soon as the tests pass.
There was a problem hiding this comment.
Note that this function is a bit weird in that I don't see any real advantage of using it in favor of using Handle.mk directly. We don't give any formal guarantees but it should be reasonable to assume that non-borrowed variables are freed (decremented) as soon as possible. And withFile doesn't guarantee that the file is closed after executing f either since the handle could be passed back in the return type. But perhaps it still gives a kind of peace of mind? @leodemoura Am I missing something?
Another complete rewrite. This implements one `ring` to rule them all: it incorporates both `ring_exp` and `ring` behaviors, now under the name `ring`. (`ring_exp` had some small (1.4x) performance issues that prevented it from being used by default; I'm hoping that those issues are fixed now, and we can revisit later if it becomes an issue.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
TODO: * Before merge - [x] fix a bug in linarith in mathlib3 I just found ... - [x] depends on: leanprover#519 - [x] style lint - [x] docs - [X] move theory stubs to a separate PR, for easier tracking: leanprover#733 - [x] failing to parse the `LinarithConfig` option * Before or after merge? - [ ] Implement the `removeNe` preprocessor. - [ ] Add support for restricting to a single type. How to store a `Type` in `LinarithConfig`? * After merge - [ ] Teach `norm_num` to solve `example [LinearOrderedRing α] : (0 : α) < 37 := by norm_num`. - [ ] Port `zify_proof` (plumbing for `zify`), and add the `natToInt` preprocessor. Mostly done now, but see leanprover#741 before all the tests will work. - [ ] Port `cancel_denoms` tactic, and add the `cancelDenoms` preprocessor. - [ ] Add the `nlinarith` preprocessor and front-end syntax. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
No description provided.