Short circuit ambiguous REPL commands

[weaversa]

Cryptol> :s
:s is ambiguous, it could mean one of:
    :sat, :set

The previous version of Cryptol would select the 'most used' command (which is subjective, but still), rather that asking the user to try again. Here, the most used command is :set for :s. It would be nice to have this back again.

[TomMD]

Whatever the preferred default might I suggest we have the defaults configurable by the user? An interface such as:

Cryptol> :s   // This is 'set'
Cryptol> :setdefault ("s","sat")  // Set prefix string 's' to expand to 'sat'
Cryptol> :s  // This is 'sat'

Should be just a simple lookup/insert in a map of defaults, which would be part of the REPL state. I expect these sorts of settings to become part of a .cryptolrc in the users home directory.

[weaversa]

I really like this idea. Also, I'm really looking forward to a .cryptolrc file.

[LeventErkok]

Argh.. I really don't like this idea :-(

It's akin to weird aliases people put in their .shellrc files, whatever that .shell happens to be. They so get used to it, if they're using somebody else's session they're completely lost! (Happens to me all the time.)

This also means that you can't just ship someone a command file, since the "commands" they have might be aliased to something else.

Of course, this is a pet peeve. Sometimes too much configurability is not a good thing. (Compare the "linux" UI experience to the "Mac" one: Former is infinitely customizable, latter is a hell of a lot better.)

I actually prefer just starting to type, like ":s" and then hit tab until it disambiguates sufficiently. Is that too much to ask?

[weaversa]

"I actually prefer just starting to type, like ":s" and then hit tab until it disambiguates sufficiently. Is that too much to ask?"
So, that currently works just fine.

[kiniry]

I, too, am not too terribly keen on an out-of-band .cryptorc . I'd rather everything be crystal-clear in the prelude and in modules. No bash- or LaTeX-like dependency hell for me, TYVM.

[acfoltzer]

We now have the ability to specify multiple aliases for the same command, so for example we have [ ":s", ":set" ] to change settings, and [ ":sat" ] to run a SAT solver. You can see all the variants by doing running :help (or, now, :?).

Note that even though we added multiple concrete aliases, if you enter an unambiguous prefix you'll still get the full command, so :sa works for SAT.

These are compiled in, rather than being user-modifiable, which we decided was too much complexity for too little benefit. We are of course open to suggestions for what the various forms should be.