Stream: Miscellaneous

Topic: ✔ Work in Scratch but not in File

Brandon Sisler (Dec 19 2022 at 22:10):

Hey all, weird question, probably simple answer.
I was trying to define some things and ran them all with scratch in the CoqIDE, and they work out fine. On the other hand, as soon as I put them into a named file, they do not work any more. I have included a simple example of this. I am not sure what's going on, I am just copying one page to another. working.PNG
not_working.PNG

Paolo Giarrusso (Dec 19 2022 at 22:16):

Ah, are you using HoTT libraries? So the second file fails because it's being compiled with the stdlib disabled?

Paolo Giarrusso (Dec 19 2022 at 22:16):

looks like the scratch file is not picking up the settings

Paolo Giarrusso (Dec 19 2022 at 22:17):

I assume you have special options for hott somewhere, like _coqproject, but where is that?

Brandon Sisler (Dec 19 2022 at 22:55):

@Paolo Giarrusso
Ha! Got me. That was it exactly. Thanks so much, I would have been at that forever.

Notification Bot (Dec 19 2022 at 22:56):

Brandon Sisler has marked this topic as resolved.

Paolo Giarrusso (Dec 20 2022 at 00:20):

I'm happy this helped!

Paolo Giarrusso (Dec 20 2022 at 00:23):

And thanks for letting me know :-)

Last updated: Jun 05 2023 at 09:01 UTC