Stream: Coq users

Topic: Library Code


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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/.

view this post on Zulip Théo Zimmermann (Nov 01 2022 at 14:33):

Examples:

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC