search

au-ts / cogent

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

AllRefine fails on master for a simple program with an abstract type #410

Open amblafont opened 3 years ago

amblafont commented 3 years ago

Consider the simple cogent program

type U7
main : U7 -> U7
main a = a

If I prepend the generated C file with typedef struct U7 { int valeur; } U7;(to give an implementation to the abstract type), AllRefine fails with the error message

Duplicate constant declaration "local.corres" vs. "local.corres"⌂
The above error(s) occurred while activating locale instance
update_sem_init "upd_abs_typing" "abs_repr"

on the line

sublocale Generated_cogent_shallow ⊆ Generated _ upd_abs_typing abs_repr
amblafont commented 3 years ago

It turns out that the issue I encountered happens when the cogent filename starts with a capital letter (whatever the content of the file is). Maybe the compiler should raise a warning in this case (or we could try to fix the bug)

zilinc commented 3 years ago

Can you elaborate why it fails with a capital letter?