search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.8k stars 642 forks source link

Request: better tutorial for Coq's module system #9745

Open luochen1990 opened 5 years ago

luochen1990 commented 5 years ago

I have finished the practices of sf/lf and part of sf/plf, and I'm familiar with many other language's module system, such as haskell/python/javascript, but still can't grasp Coq's module system, I think it is the most complex one.

To learn Coq's module system, I read the following resources:

First is the official doc, it's all about definition of abstract noun and formulas, and tells nothing about the situation and usage. I felt helpless.

Then I go to the wiki, it start with telling me how to write my own module. but why I need to write a module for just min and max, and what is the name Sig for? and why there is utf8 ?

The most important things is, I still have a lot of basic problems about Coq's modules, but these tutorial tells nothing about them, e.g.

  1. How can I find a module I want? by name? by type? via google? is there a site similar to hoogle for haskell ?
  2. How to use an existing module I found? what's the different between Import/Require?
  3. What is the relationship between Module and Scope?
  4. How does Coq organize it's internal modules? what is the principle?

I think there should be a better ModuleSystemTutorial which focus on "how to use modules" instead of "how to write modules", I think it will help Coq newbies a lot and make them fell less helpless.

Zimmi48 commented 5 years ago

This kind of question is better asked on Coq's Discourse forum at https://coq.discourse.group.

Zimmi48 commented 5 years ago

The module chapter of the reference manual is pretty horrible indeed as it is only about typing rules.

zStruCat commented 1 year ago

Any progress on this matter? It seems that most books on coq covers little about module and build......

thomas-lamiaux commented 2 months ago
  1. How can I find a module I want? by name? by type? via google? is there a site similar to hoogle for haskell ?
  2. How to use an existing module I found? what's the different between Import/Require?
  3. What is the relationship between Module and Scope?
  4. How does Coq organize it's internal modules? what is the principle?

It seems to me that:

  1. X
  2. I do not know what is in the refman, but this is now covered by the tutorial require import
  3. I do not know what is in the refman, but I guess it could be covered by a tutorial
  4. It seems like a refman matter