Please use qualified paths in the example files

[MSoegtropIMC]

Dear CoRN Team,

the example files, like examples/RealFaster.v require CoRN modules without qualification. This doesn't work if CoRN is installed as opam package, so users have to patch the examples in order to run them. It also makes it hard to find usable "smoke test kit" files for Coq Platform.

Best regards,

Michael

[spitters]

I believe there is a tool that can do this, isn't there?
I'd be happy to merge a PR. I don't know when I have time to do it myself.

[Zimmi48]

Probably that one: https://github.com/JasonGross/coq-tools/blob/master/absolutize-imports.py

[MSoegtropIMC]

@spitters : I have issues compiling examples after fixing the require paths. E.g. when I prepend CoRN.reals.fast to the requires in PlotExample.v, I get an error on the Time Eval vm_compute in PlotQ ...:

The term "∗" has type "Lt = Lt" while it is expected to have type "Qpos".

[spitters]

Could it be a scope problem?

…

On Wed, Jan 26, 2022 at 10:58 AM MSoegtropIMC ***@***.***> wrote: @spitters <https://github.com/spitters> : I have issues compiling examples after fixing the require paths. E.g. when I prepend CoRN.reals.fast to the requires in PlotExample.v, I get an error on the Time Eval vm_compute in PlotQ ...: The term "∗" has type "Lt = Lt" while it is expected to have type "Qpos". — Reply to this email directly, view it on GitHub <#162 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTWUWAWSWXRKVARWIG3UX7AVJANCNFSM5EV5IJYQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you were mentioned.Message ID: ***@***.***>

[MSoegtropIMC]

Could it be a scope problem?

Likely. I could very likely fix it myself - I am just a bit busy with the Coq Platform release.