search

AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
104 stars 6 forks source link

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

Closed dalybrown closed 8 months ago

dalybrown commented 8 months ago

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 commented 8 months ago

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 commented 8 months ago

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 commented 8 months ago

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