Robert Watson (Nov 01 2022 at 14:17): Robert Watson (Nov 01 2022 at 14:17):I've very recently started learning Coq. I can't find the standard library code on GitHub. For example there is this : https://coq.inria.fr/library/Coq.Logic.FunctionalExtensionality.html
But it isn't a .v file or anything. It's a mere rendering (and maybe not complete/uptodate - and in any case I would like to see the real code). I thought it would be here:
https://github.com/coq/coq/tree/master/library
But it isn't.
So I thought it was installed externally, via this:
https://github.com/coq/platform
But I can't find what I'm looking for. So I'm obviously doing something dumb. Please help!
walker (Nov 01 2022 at 14:19):I think the library you are looking for is located here:
https://github.com/coq/coq/tree/master/theories
inside coq's source code
Robert Watson (Nov 01 2022 at 14:28):Thanks. And in particular this:
https://github.com/coq/coq/blob/master/theories/Logic/FunctionalExtensionality.v
"theories" huh? OK. I can get used to that!
Théo Zimmermann (Nov 01 2022 at 14:32):It's not just the standard library that uses this terminology. You will find that many Coq packages have a theories/ directory as well. And when there is a src/ directory and a theory/ directory, it usually means that this is a plugin and the OCaml code is in src/.
Théo Zimmermann (Nov 01 2022 at 14:33):Examples:
Robert Watson (Nov 01 2022 at 14:39):Got it. And I should use the same.
I'm uncomfortable about the use of 'Axiom' in https://github.com/coq/coq/blob/master/theories/Logic/FunctionalExtensionality.v, much as I will probably use it. But how do you know you haven't imported a (non-Core) Axiom you don't want, or don't even know about? Or, more subtly, have imported (Require'd!) some code or a proof that uses such an Axiom somewhere deep inside? I mean, you don't want to have to look through imported files and all dependencies to make sure you haven't added Axioms unconsciously, right?
Karl Palmskog (Nov 01 2022 at 14:52):if you use coq_makefile to generate your Makefile as in coq-mmaps, you can run make validate and see what axioms you're using. If the axioms you use are defined in Coq.Logic, you're fine w.r.t. consistency (to the best of what people currently know)
Karl Palmskog (Nov 01 2022 at 14:59):see section 4.1 in this document for advice on how to think about axioms and hypotheses in Coq
Ana de Almeida Borges (Nov 02 2022 at 08:22):You can also Print Assumptions lemma_name. to see which axioms were needed for that particular lemma
Last updated: Apr 18 2024 at 14:02 UTC