search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Inconsistent syntax of type table? #376

Closed gteege closed 3 years ago

gteege commented 4 years ago

The format of the table generated by cogent --table-c-types seems to be incompatible with the parser in cogent/c-refinement/ReadTable.thy. This causes _CorresSetup.thy files to fail when run by isabelle.

vjackson725 commented 3 years ago

Could you give an example of a failing type-table? Also, are you using dargent or not?

gteege commented 3 years ago

When preparing the example I found the reason: Caused by the change to the new cabal I was stuck with a Cogent binary from an old version. Using that together with the new Cogent distribution caused the inconsistency. After cleaning that up everything runs smoothly. Sorry for the inconvenience.