REPL command line syntax / mode transitions

[thedotmatrix]

1. Our command syntax doesn't really conform to some "style". The commands are all over the place. Some are single letters, some are full words. Shorthand commands are nice, but knowing something such as "all commands are symbols then a letter" or "all commands are one/two words all lowercase" will make it easier to type / more intuitive for a user.
2. Explicitly saying "take me to mode X" is really annoying to type. Either define explicit commands for the transition (@m means nothing; explore does though), or transition implicitly (user asked to load a theory in some other mode, automatically go to theory mode instead of syntax error), or a combination of both. I'm a fan of the implicit transitions. The user should be able to know / call every command at all times; however, the "modes" should still be displayed to the user in the hopes to get them in the right mindset.
3. because i think its going to be highly related to this change, adding a "pipe" for REPL output would be nice. that is, some interface that will allow for interchangeable output (either stdout which is the only current implementation, opening up the output as a text file in an editor, xml, json).

@salmans @dandougherty now that we've gotten some feedback on the modes, and in general i think its a good idea, would this be the time to really formalize our command syntax? (maybe even a technical report / the start of a bigger paper?)

[dandougherty]

On Tue, Dec 9, 2014 at 11:25 PM, Ryan Danas notifications@github.com
wrote:

would this be the time to really formalize our command syntax? (maybe even
a technical report / the start of a bigger paper?)

I say yes, then no. That is, formalize it as it stands now, which will
help squeeze out out infelicities, but we need a little more user feedback
before we freeze it into something we write a report about.

[salmans]

Again, I agree. I think it will take a while and a lot of feedback from our users to get the interface right.

[thedotmatrix]

The modes did a good job of breaking up the repl into separate states; I currently like the following idea for transitions...

• User starts in a "current mode"
• User gives command for any mode
• REPL figures out what mode it's related to
• REPL automatically transitions to that mode and executes the command
• That mode may update what the "current mode" is, from where the user started
• REPL will automatically transition back to whatever the "current mode" is set to

This would work really nice with changing theory configuration options (like depth), as it would transition to theory mode, change the depth, transition to the model exploration mode, and reload the theory / generate the first model automatically.

[dandougherty]

Yes, I like the spirit of this idea. I read it as
(i) we have different modes, essentially a "typing discipline" for the
REPL commands,
but
(ii) we don't burden the user with the tedium of changing modes in order to
execute a command.

It's a bit like type inference for REPL commands, isn't it? It's mode
inference.
As long as the commands appropriate to different modes are orthogonal
enough the user will always know, maybe subconsciously, which mode she
intends to be in.

Dan

On Sat, Jan 24, 2015 at 1:31 PM, Ryan Danas notifications@github.com
wrote:

The modes did a good job of breaking up the repl into separate states; I
currently like the following idea for transitions...

• User starts in a "current mode"
• User gives command for any mode
• REPL figures out what mode it's related to
• REPL automatically transitions to that mode and executes the command
• That mode may update what the "current mode" is, from where the user
  started
• REPL will automatically transition back to whatever the "current
  mode" is set to

This would work really nice with changing theory configuration options
(like depth), as it would transition to theory mode, change the depth,
transition to the model exploration mode, and reload the theory / generate
the first model automatically.

Reply to this email directly or view it on GitHub
#56 (comment).