Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

coqdoc -g omits "Declare Instance" #2389

Closed
coqbot opened this issue Sep 18, 2010 · 5 comments
Closed

coqdoc -g omits "Declare Instance" #2389

coqbot opened this issue Sep 18, 2010 · 5 comments
Assignees
@herbelin
Labels
part: coqdoc The coqdoc binary for building documentation. part: tools Coqdoc, coq_makefile, etc.

Comments

@coqbot
Copy link
Contributor

coqbot commented Sep 18, 2010

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2389
From: Yevgeniy Makarov <emakarov@gmail.com>
Reported version: trunk
CC: @herbelin
@coqbot
Copy link
Contributor Author

coqbot commented Sep 18, 2010

Comment author: Yevgeniy Makarov <emakarov@gmail.com>

The following is a part of the Coq.Structures.Equalities library.

Module Type IsEq (Import E:Eq).
Declare Instance eq_equiv : Equivalence eq.
End IsEq.

However, the output of coqdoc -g (and, therefore, the generated HTML library listings) contain only

Module Type IsEq (Import E:Eq).
End IsEq.

I have trunk 13419.

@coqbot
Copy link
Contributor Author

coqbot commented Sep 19, 2010

Comment author: @herbelin

Hi Evgeny, I fixed it (by adding explicitly Declare Instance as a command, r13440) but the fix is not robust since option -g removes all the commands that are not known explicit known from coqdoc, leading to permanent coqtop/coqdoc synchronisation problems. Thus I let the report open.

@coqbot
Copy link
Contributor Author

coqbot commented Jun 7, 2017

Comment author: @Zimmi48

Hugo, what is the status of this? Is the bug still worth to be left open? If there is a general issue with coqdoc, maybe a new bug report explaining it would be more suited?

@coqbot
Copy link
Contributor Author

coqbot commented Jun 8, 2017

Comment author: @herbelin

Hugo, what is the status of this?

The "Declare Instance" case is fixed (https://coq.inria.fr/distrib/current/stdlib/Coq.Structures.Equalities.html#IsEq).

Is the bug still worth to be left open? If
there is a general issue with coqdoc, maybe a new bug report explaining it
would be more suited?

Yes, maybe a new bug would be better. Maybe worth also to see if Yann can explain us his new almost finished but not fully finished coqtop-based coqdoc.

@coqbot coqbot added the part: tools Coqdoc, coq_makefile, etc. label Oct 18, 2017
@SkySkimmer
Copy link
Contributor

Yes, maybe a new bug would be better.

Let's close this one then.

@Zimmi48 Zimmi48 added the part: coqdoc The coqdoc binary for building documentation. label Apr 5, 2020
gmalecha pushed a commit to bluerock-io/coq that referenced this issue Dec 12, 2024
Fixing bug coq#2389 (keyword "Declare Instance" unknown from "coqdoc …
582658a 
…-g") but

this lacks robustness since "coqdoc -g" will drop away any commands unknown
from coqdoc, leading to possible synchronisation problems.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13440 85f007b7-540e-0410-9357-904b9bb8a0f7
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@herbelin herbelin

Labels
part: coqdoc The coqdoc binary for building documentation. part: tools Coqdoc, coq_makefile, etc.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@herbelin @Zimmi48 @SkySkimmer @coqbot