How to use the REPL mode of sail?

[wanghuibin0]

I found that Sail has a REPL mode, which provides users with an interactive command line.
However, I didn't understand how to use this REPL, even after checking the output of the :help command.
Is there a complete example to illustrate how to use this REPL? Additionally, what is the design purpose of this REPL?

[trdthg]

Does sail have a REPL mode? (just curious)

[Alasdair]

Yes, sail -i opens an interactive interpreter. It's not super useful because you can't load files at runtime, so you have to start it as sail -i <files> as if you were building the model, and it also checks all the files beforehand so the startup time is quite slow.

I would like to change it so it can type-check the provided files lazily as expressions are executed which would reduce the startup time.

[rmn30]

I've found it useful for stepping through property counterexamples returned by the SMT backend.

[Timmmm]

I'd really appreciate some documentation for this interface. It seems to have quite a confusing mode system...

sail> :commands
Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :prove :assume :clear :commands :help :output :option
Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :recheck :compile :sail_dir :bin :elf :graph :thin_slice :slice :slice_cuts :slice_keep_std :slice_roots :symbols :undef_symbol :define_symbol :specialize :target :rewrites :list_targets :list_rewrites :fix_registers
Evaluation mode commands - :(r)un :(s)tep :step_(f)unction :(n)ormal

:(c)ommand can be called as either :c or :command.
sail> :load
Command :load is not a valid command in this mode.
sail> :run
Command :run is not a valid command in this mode.
sail> :normal
sail> :load
Command :load is not a valid command in this mode.

The :commands help implies it has two modes, Normal and Evaluation, but the :load and :run error messages suggest it isn't in either mode, even after :normal seems to succeed?

[Alasdair]

The :load doesn't exist anymore as it behaved weirdly with scattered definitions - :load f1 followed by :load f2 was not the same as :load f1 f2. Right now you pass the files on the command line with sail -i f1 f2. I'll adjust the help output in the REPL.

I would like to add that command back in but it needs a bit of work to make it behave sensibly.