coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Installation

From: Anthony Bordg <bordg.anthony AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Cc: Anthony Bordg <bordg.anthony AT gmail.com>
Subject: Re: [Coq-Club] Installation
Date: Fri, 10 Feb 2017 18:08:22 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bordg.anthony AT gmail.com; spf=Pass smtp.mailfrom=bordg.anthony AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f53.google.com
Ironport-phdr: 9a23:/kj9rhU6nQhfVf30eofgD2R8Su3V8LGtZVwlr6E/grcLSJyIuqrYbBSBt8tkgFKBZ4jH8fUM07OQ6PG8Hzxfqsfd+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe71/IRG5oAnLtcQbg4RuJ6I+xxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjk2/nzKisxrlKJUvg6upwBxzY7TZYGaLvt+fqXAdt8eSmdMWsNdWipcCY2+coQPFfIMMuRWr4f9qVUArgawCxewC+700DBEmmX70Lcm3+g9EwzL2hErEdIUsHTTqdX4LLsfUeapzKnIyjXDafNX0irg5YjPaBAuvP6MVq93fMXKzkkvDR7KjlqKpYP/OTOVyuQNs2+d7+tgTu+vhGsnpBtwojir3Msjlo7JhocMx13C6C53zoE1JdiiR056Z96pCJRQtyadN4t5RsMtXXtktzo9yr0Dv5OwYSsEyIw/yhLBd/CKd5KE7xHjWeqLPzt0mXFodKi/ihu890Wr1/fyWdOu0FlQqypIitnMuW4J1xzU8sWHT+Fy/kal2TqW0ADT6/1ILVk6lafbJZMt2LEwlp0UsUTMGi/5hl/6g7ORdkUh4uSo6uLnbav6ppKEKYN4lgXzPr4tl8G/G+g0LBUCUmuB9em82rDv5Uj5T69Ljv0ynKnZqpfaJcEDq6GiBA9VyJss6xmlAzi81tQYgXkHLFVDeBOHlIXpNFTOL+r5Dfe7mVijjDBrx/XeMr37HprNNmTDkKvmfbtl90FczxMzwclD6JJQF7EOO+n+WlTxtdzdFh82KRa4w+fhCNVn14MRQ3iDAqGDMPCajVjd7eU2ZuKIeYVd7D36Mr0u4+PkpX4/g14UO6ezi8g5cne9S91gP0WeZ2ukqNAbHWhC6gA5VuDlzlSETT5UYWeaUKc15zV9A4WjW9SQDruxiaCMiX/oVqZdYXpLXwzdHA==

Hi Théo,

2017-02-10 17:40 GMT+01:00 Théo Zimmermann <theo.zimmi AT gmail.com>:

When you say "I installed", you mean "I build from source", right?

yes, build from the source

What configuration options did you use? ./configure -local?

I used "./configure -local", with no further option.

When you say "I tried to process a file", you mean a file from the theories/ folder right?

yes, a file from the "theories" folder (using CoqIDE)

If the answer to all these questions is yes, then I've been observing the same problem when trying to improve some theories files (with Emacs/Proof-General too). I wanted to ask around what this was about but did not get to do it yet. However, not being an expert on these matters, I'm afraid I can't help further.

PhD. Anthony Bordg

postdoctoral fellow

Mathematical Institute Charles University
https://sites.google.com/site/anthonybordg/

[Coq-Club] Installation, Anthony Bordg, 02/10/2017
- Re: [Coq-Club] Installation, Théo Zimmermann, 02/10/2017
  - Re: [Coq-Club] Installation, Anthony Bordg, 02/10/2017
    - Re: [Coq-Club] Installation, Christian Doczkal, 02/10/2017
- RE: [Coq-Club] Installation, Soegtrop, Michael, 02/10/2017
  - Re: [Coq-Club] Installation, Anthony Bordg, 02/10/2017