Save and load REPL context via :save and :load commands #807

basile-henry · 2019-01-31T10:14:35Z

This PR closes #706

The format for the save file is a plain Dhall file where we expect the normal form to be a record literal. This will hopefully mean that the save file can be edited manually if need be without too much effort.

The save files are always kept by default (their index is incrementing) and only the last one is loaded by default.

It is possible to manually specify where to save and load the context to.

basile-henry · 2019-02-01T04:25:01Z

I am not sure why hydra is failing, I can build this with nix-build just fine.
It seems to be complaining that listDirectory is not being exported by System.Directory, but it has been there since version 1.2.5.0 according to the haddock comment.
Any idea what might be happening?

Gabriella439 · 2019-02-01T15:23:11Z

@basile-henry: It's because CI builds dhall against GHC 7.10.3 which requires a specific (old) version of the directory library

Gabriella439

Looks great! Just one comment

Gabriella439 · 2019-02-01T15:31:07Z

dhall/src/Dhall/Repl.hs

+
+  saveBinding [file]
+
+-- Save all the bindings into a big record into `file`


We probably should use something other than a record to store the bindings because we need to preserve the original order. The context permits duplicate entries and if their order is switched then you change which one shadows which

I saw that the context keeps the shadowed bindings, but I'm not too sure why.

Maybe if we weren't normalizing the bindings before adding them to the context then we would need to have access to the shadowed bindings. But I believe that when we normalise while adding a new binding, it gets rid of any dependencies on previous bindings, or is that not the case?

Or maybe we need access to the shadowed bindings for something else?

The current solution I have is to only serialise the version of a binding accessible to the user when they type :save.

@basile-henry: It's still possible to refer to shadowed bindings using the @n suffix, like this:

⊢ :let x = 1 x : Natural ⊢ :let x = True x : Bool ⊢ x@1 1

Ah, I didn't know about this feature.

I liked the idea of using dhall to serialise the REPL state. What would you recommend as a format?

I could use [ { name : Text, expr : Text } ] but then the save file can't really be used for anything else.

This isn't just a feature of the REPL! It's a Dhall thing, where can I find the documentation about it?

➜ dhall <<< "let a = 1 let a = 2 in a@1" 1

Ok, about the serialization format, I thought about it a bit more. Maybe I shouldn't use Dhall to serialize the context and instead serialize the context like entries a user could input into the REPL.

Something like:

:let x = 2 :let x = 3 :let y = "foo" :let z = x + 5

My reasoning for this is that it makes the :load command more general than just loading a saved state of the context. This format is similar to the format used by a .ghci file. We could imagine in the future automatically loading such a file (maybe named .dhall-repl) on startup, but that's a separate issue.

What do you think of this idea? In my previous suggestion of [ { name : Text, expr : Text } ] I really disliked serializing Dhall expressions as Text.

I'll get started with this idea, but do tell me if you think it's not the right way to solve this issue! 😄

Also, I'm not too sure what to do with stdout when replaying these :let commands, it could get noisy very fast...

jneira · 2019-02-01T16:01:19Z

Strangely the appveyor build with ghc-7.10.3 succeded 🤔
https://ci.appveyor.com/project/Gabriel439/dhall-haskell/builds/22043719/job/kkc0tg9w4d46pv4c

The format for the save file is a plain Dhall file where we expect the normal form to be a record literal. This will hopefully mean that the save file can be edited manually if need be without too much effort. Signed-off-by: Basile Henry <bjm.henry@gmail.com>

The format used is the set of commands needed to recreate the saved context. When loading a saved file, the output emitted by replaying the commands is discarded. This commit also adds file autocomplete to the load command. Signed-off-by: Basile Henry <bjm.henry@gmail.com>

basile-henry · 2019-02-02T08:54:04Z

dhall/src/Dhall/Repl.hs

+            (env { outputHandle = nullHandle })
+
+  -- Use a null handle (to discard output) to run all the commands
+  newEnv <- liftIO $ System.IO.withFile "/dev/null" System.IO.WriteMode handler


I have no idea how platform independent this solution is. Any pointers to improve this? Or do you think this works on Windows somehow? 🤞

Appveyor is happy so it works in windows 👍

Unfortunately I don't think Appveyor runs the REPL, and this will likely be a runtime error 😅

oh right, i forgot that sometimes it compiles but fails at runtime. It seems that it will fail in windows, yes.

I've tested the pr in my windows env and i've not been able to trigger any error. The steps were:

run the dhall repl

type some binding: :let a = 1

:save the session

:load the session

quit and rerun repl and load the session again

Because of the withFile pattern, if there's an error in the handle. It probably just skips the loading bit

Thanks for testing, I'm still surprised it doesn't crash. Could you try to exit in between save and load? And the check if a is in scope.

My last test was just that, including the console output to be more precise:

D:\dhall-haskell>stack run dhall -- repl ⊢ :let a = 1 a : Natural ⊢ a 1 ⊢ :save Context saved to `.dhall-repl-0` ⊢ :quit Goodbye. D:\dhall-haskell>stack run dhall -- repl ⊢ :load Loaded `.dhall-repl-0` ⊢ a 1

I am on windows 10, not sure if it would work in older systems.
Maybe the solution ib this so answer could be applicable here: https://stackoverflow.com/a/41527205/49554

Ah thank you! If hSilence is properly cross platform I could use that. Otherwise I could use a Maybe Handle as part of the state instead and just not print anything when I don't have a handle.
That might be cleaner! 😄

Yeah, I would configure the REPL so it can optionally not print output when replaying commands

Gabriella439 · 2019-02-03T04:33:38Z

dhall/src/Dhall/Repl.hs

@@ -75,6 +79,7 @@ data Env = Env
  , explain          :: Bool
  , characterSet     :: CharacterSet
  , _standardVersion :: StandardVersion
+  , outputHandle     :: Maybe System.IO.Handle


Perhaps instead of storing a Maybe System.IO.Handle you can store a Text -> IO (). Then when you want to write something you set it to Data.Text.IO.putStrLn and when you want to output nothing you set it to mempty

We also use renderIO to pretty print Dhall, which uses the handle.
I could add an extra rendering function similar to what you suggest, as part of the state, but the Maybe Handle seems lighter. What do you prefer?

Would it be possible to still use renderIO if you change the Env to store a function of type Doc -> IO () instead?

Gabriella439 · 2019-02-12T05:50:07Z

I'll go ahead and merge this. If we need any additional changes I can make them in a subsequent pull request

basile-henry self-assigned this Jan 31, 2019

basile-henry force-pushed the basile/repl-save branch from 83c4f2b to cbf5a99 Compare February 1, 2019 03:29

Gabriella439 reviewed Feb 1, 2019

View reviewed changes

basile-henry added 3 commits February 2, 2019 14:06

Use getDirectoryContents instead of listDirectory

94cf8eb

basile-henry force-pushed the basile/repl-save branch from 20b6d13 to 2e4f731 Compare February 2, 2019 08:52

basile-henry commented Feb 2, 2019

View reviewed changes

Use a Maybe Handle instead of a null handle for output logic in REPL

93e31c8

Gabriella439 reviewed Feb 3, 2019

View reviewed changes

Merge branch 'master' into basile/repl-save

71ebf7b

Gabriella439 merged commit d20b1ca into master Feb 12, 2019

Gabriella439 deleted the basile/repl-save branch February 12, 2019 06:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Save and load REPL context via :save and :load commands #807

Save and load REPL context via :save and :load commands #807

basile-henry commented Jan 31, 2019 •

edited

Loading

basile-henry commented Feb 1, 2019

Gabriella439 commented Feb 1, 2019

Gabriella439 left a comment

Gabriella439 Feb 1, 2019

basile-henry Feb 1, 2019 •

edited

Loading

Gabriella439 Feb 1, 2019

basile-henry Feb 1, 2019

basile-henry Feb 2, 2019

jneira commented Feb 1, 2019 •

edited

Loading

basile-henry Feb 2, 2019

jneira Feb 2, 2019

basile-henry Feb 2, 2019

jneira Feb 2, 2019 •

edited

Loading

jneira Feb 2, 2019

basile-henry Feb 2, 2019

jneira Feb 2, 2019

jneira Feb 2, 2019 •

edited

Loading

basile-henry Feb 2, 2019 •

edited

Loading

Gabriella439 Feb 2, 2019

Gabriella439 Feb 3, 2019

basile-henry Feb 3, 2019

Gabriella439 Feb 4, 2019

Gabriella439 commented Feb 12, 2019


		saveBinding [file]

		-- Save all the bindings into a big record into `file`

Save and load REPL context via :save and :load commands #807

Save and load REPL context via :save and :load commands #807

Conversation

basile-henry commented Jan 31, 2019 • edited Loading

basile-henry commented Feb 1, 2019

Gabriella439 commented Feb 1, 2019

Gabriella439 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

basile-henry Feb 1, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jneira commented Feb 1, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jneira Feb 2, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jneira Feb 2, 2019 • edited Loading

Choose a reason for hiding this comment

basile-henry Feb 2, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Gabriella439 commented Feb 12, 2019

basile-henry commented Jan 31, 2019 •

edited

Loading

basile-henry Feb 1, 2019 •

edited

Loading

jneira commented Feb 1, 2019 •

edited

Loading

jneira Feb 2, 2019 •

edited

Loading

jneira Feb 2, 2019 •

edited

Loading

basile-henry Feb 2, 2019 •

edited

Loading