Command line switch rflx --no-verification --unsafe generate doesn't seem to work

[dalybrown]

I might not understand the purpose of the --no-verification --unsafe so you can delete this issue if that is the case.

There are times I want to speed up the generation of the SPARK code from our model when I know the model has already been checked and verified and the code proved (e.g., when the it is used as a dependency in another project).

I thought this switch would skip the Verifying ... part of the generate command. However, I still see those steps output every time I run the command with that switch which leads me to believe the switch isn't doing anything or the output is incorrect.

Please advise - thanks!

[treiher]

Your expectation is correct, the output is just misleading. Despite the Verifying ... output, no verification is done when --no-verification is used. We will fix this. Thanks for reporting this!

Note that it is not necessary to use --no-verification if the verification has already been done on the same machine. The successful verification result will be cached (in $HOME/.cache/RecordFlux) and the verification will be skipped on the next run. Caching is only done for messages and refinements, as the verification time for other declarations is negligible.

[dalybrown]

Thanks!

Actually it's for CI pipelines that we use it when we know it has previously been verified but we might not have a cache available to us.

[treiher]

This is now fixed on main and will be part of version 0.18.0.