easyuc / EasyUC

Experiments with Universal Composability in EasyCrypt
31 stars 1 forks source link

batch mode for .uci files should be silent unless an error happens #28

Closed alleystoughton closed 1 year ago

alleystoughton commented 1 year ago

I think that batch model for .uci files should be silent unless an error happens, exiting with status 0 when it succeeds, and status 1 when an error happens. That way it can be used in this mode in a continuous integration testing framework.

Also, at the moment, it infinite loops at the end of a .uci file:

parse error
#28>
[error: testing-ideal.uci: from line 99 columns 1 to 1]

parse error
#28>
[error: testing-ideal.uci: from line 99 columns 1 to 1]

parse error
#28>
[error: testing-ideal.uci: from line 99 columns 1 to 1]

parse error
#28>
[error: testing-ideal.uci: from line 99 columns 1 to 1]

parse error
#28>
[error: testing-ideal.uci: from line 99 columns 1 to 1]

parse error
#28>
[error: testing-ideal.uci: from line 99 columns 1 to 1]

parse error
#28>
[error: testing-ideal.uci: from line 99 columns 1 to 1]

parse error
alleystoughton commented 1 year ago

Reopening this because execution is not silent, and although running ucdsl testing-ideal.uci doesn't infinite loop, it does terminate (incorrectly) with a syntax error:

input guard: 16 control: environment Message was output: environment: ((func, 1))@SMC2.SMC2Dir.Pt1.smc_rsp(text)@(([], 1)) ;

28>

28>

[error: testing-ideal.uci: from line 99 columns 1 to 1]

parse error