Discourse Bot (Jun 18 2020 at 16:49): Discourse Bot (Jun 18 2020 at 16:49):Łukasz Czajka @lukaszcz posted in Converting an Ltac tactic to Proofview.tactic
Suppose I have tactic TAC declared in a *.v file by Ltac TAC args := … I want to access it in a plugin at the OCaml level as a Proofview.tactic. What is the best way to do this?
In particular, if TAC takes a constr argument, how do I convert it to Proofview.tactic so that I can feed it a Constr.t or EConstr.t? This is the case I’m most interested in. If there are no arguments or the arguments are...
Théo Zimmermann (Jun 18 2020 at 16:50):(The above is not really "new" but a test that the Discourse integration correctly works.)
Discourse Bot (Jun 28 2020 at 09:30):Haruka Kawamura @itleigns posted in Real number without axiom
Hello everyone.
I composed real number without using any axioms other than that of logic. Is this useful for the community?
Discourse Bot (Jul 08 2020 at 13:14):@ZWY posted in Confused with qualid
By definition of Coq documentation,
Identifiers may also denote local variables, while qualified identifiers do not.
It is no problem to say that “qualid denotes global objects”.
However, I found in the tactic apply H, H is a qualid and also a local variable contradicted to the
documentation.
So my question is whether it is precise enough to say “qualid denotes global objects”.
To be more p...
Discourse Bot (Jul 12 2020 at 12:41):@ZWY posted in The tactics denoted by qualid
I know there are some tactics denoted by qualid like split and destruct. Do all of such tactics are written in the file coretactics.mlg?
Discourse Bot (Jul 24 2020 at 18:40):Théo Zimmermann @Zimmi48 posted in The V8.12.0 tag has been created
Dear packagers,
This is an early announcement that the V8.12.0 tag has been created
and that it is time to package Coq for the various distributions /
package repositories.
The official announcement of the release should come soon.
Cheers,
Emilio and Théo, your 8.12 release managers
Discourse Bot (Jul 27 2020 at 19:00):@randair posted in "Running" Proofview.tactic to see if it would succeed
I’m writing a plugin that suggests a sequence of tactics to copy-and-paste into my proof.
I would prefer not to generate tactics that fail. My idea is to first build the Proofview representation of these tactics, and then to silently “execute them” on a goal/environment. If it fails, my plugin is to consider different tactics.
Is this possible?
Discourse Bot (Jul 27 2020 at 21:19):@randair posted in Can you pass tactics to a plugin?
Is it possible for a plugin command to get tactic scripts as input?
I would imagine this is possible since try accepts an Ltac expression.
Discourse Bot (Aug 17 2020 at 21:31):@randair posted in Proofview.tactic to string or Pp.t
Is there a way to print a Proofview.tactic as an Ltac expression?
Discourse Bot (Sep 13 2020 at 18:34):Gert Smolka @gert-smolka posted in Historical questions concerning inductive types (guard condition, accessibility)
Dear Coq pioneers and experts,
I’m curious about two issues with inductive types that changed since Giménez tutorial (1998; 2006 with Pierre Castérand) and the Coq’ Art Book (2004, Coq V8.0)In the Ssreflect tutorial (2009) a direct definition of an Euclidean division function appears exploiting an extended guard condition. This is in sharp contrast to Giménez’ tutorial and the Coq’ Art book ...
Discourse Bot (Oct 13 2020 at 06:03):Andrej Dudenhefner @mrhaandi posted in Ad hoc asynchronicity
In large, complex proofs it is sometimes difficult to make the overall argument parallel (due to linear Require dependencies). However, it is common practice in individual proofs to see e.g.
apply lemma1; [ auto | firstorder | ].
apply lemma2; [ trivial | auto | ].
rest_of_proof...In particular, applying lemma1 and lemma2 creates several (here three) subgoals, of which only one (here the third)...
Discourse Bot (Nov 04 2020 at 14:34):Enrico Tassi @gares posted in Dates for the 8.13 release
Dear Coq developers,
with our release manager hat on we communicate the following
dates:
Freeze: 16 November
Beta: 7 December
Final: 7 January
Given the current working constraints, we'd love to keep the number of
PRs to backport as low as possible: ideally only user facing bugs and
doc updates.
Best regards,
Discourse Bot (Nov 05 2020 at 14:56):@ZWY posted in Recommended resource for developing Coq plugin
I have been working on developing Coq plugins for more than one year.
However, I am still struggling with the architecture of Coq source code and often can not find suitable functions inner Coq to implement my ideas.
The only resource explaining the Coq architecture found by me is
https://www.dc.fi.udc.es/staff/freire/coqdoc/pauillac.inria.fr/coq/doc/n111.html, which is developed in 1998 and ve...
Discourse Bot (Nov 11 2020 at 05:50):@Lasse posted in How to properly configure the ML load path for ocaml packages in opam projects
Hi Everyone,
I’m trying to create a plugin that has dependencies on external OCaml packages. I am aware of the linking issues with this, but using dune I can compile my plugin with relative ease.
The problem occurs when I actually try to use my plugin. If I try to load the master .vo file of my plugin, I encounter ML loadpath errors. Coq cannot find the libraries I am referencing using Declare M...
Discourse Bot (Nov 13 2020 at 17:13):Théo Zimmermann @Zimmi48 posted in The V8.12.1 tag has been put
This message is to inform package managers that the V8.12.1 tag has
been put and it is time to update Coq in your favorite package
repository / registry.
A proper announcement of the release will follow (probably on Monday)
once the Windows installers are signed.
Thanks!
Your 8.12 release managers, Emilio and Théo
Discourse Bot (Dec 11 2020 at 08:56):Théo Zimmermann @Zimmi48 posted in The V8.12.2 tag has been set
This message is to inform package managers that the V8.12.2 tag has
been set and it is time to update Coq in your favorite package
repository / registry.
A proper announcement of the release will follow (probably on Monday).
This initially unplanned release is in response to two impacting 8.12
regressions that were only discovered and fixed after the 8.12.1
release.
Thanks!
Your 8.12 relea...
Discourse Bot (Mar 24 2021 at 13:31):Arthur Charguéraud @charguer posted in Generalizing coercions to infer typeclass arguments
The following example, using inhabited types, motivates the potential interest for allowing coercions to leverage typeclass inference. I wonder if there would be obstacles to supporting it.
Set Implicit Arguments.Class Inhab (A:Type) : Prop :=
{ inhab: exists (x:A), True }.Record IType : Type := IType_make
{ IType_type :> Type;
IType_inhab : Inhab IType_type }.Arguments IType_make I...
Discourse Bot (Mar 30 2021 at 02:41):Gregg Reynolds @mobileink posted in Building Coq with Bazel - need help with plugins
Hi folks. I’m almost done building the OCaml parts of Coq with OBazl. Caveat: OBazl is new and undergoing some changes, so the docs are a little outdated.
I’ve run into problems building some of the plugins. I posted a message to the Coq channel of the OCaml discord server. Which is the most appropriate forum?
I will also need some help with the next phase, which is building the .v files. I ...
Discourse Bot (Apr 02 2021 at 09:48):Théo Zimmermann @Zimmi48 posted in Our code of conduct might be incomplete
Over the past couple of weeks, I have been a witness of several
written discussions between regular contributors that created
frustration or led to aggressive comments. I have also been pointed to
several others, which I would otherwise have missed.
These situations are counterproductive because they frequently lead to
at least two contributors feeling discouraged, or even accumulating
grief...
Discourse Bot (Apr 27 2021 at 08:08):Théo Zimmermann @Zimmi48 posted in Dune is now required to build Coq
Dear Coq developers and contributors,
I'm about to merge PR (when CI passes one last time)
[build] Use dune to build OCaml code. by ejgallego · Pull Request #13617 · coq/coq · GitHub "Use dune to build OCaml code".
This means that from now on, Dune (>= 2.5.1) becomes mandatory for
building Coq (though Dune >= 2.8.5 is recommended).
We still have two build systems at this point: one that uses ...
Discourse Bot (May 10 2021 at 14:32):@Nifrec posted in Ltac2: Function to match a variable with a type
Dear Coq community,
I have been trying to write a function in Ltac2 that takes two arguments:a constr ‘x’ that can be of any type
a constr ‘t’ that is a TypeI want this function to give different output if ‘x’ belongs to the Type of ‘t’ than in the case in which it does not.
The following is a minimal example of the best I managed to produce so far.
However, it does not work as intended. &t...
Discourse Bot (May 21 2021 at 08:46):@AoS posted in Ltac2: checking if an optional input variable is present
Dear community,
I am working with Ltac2 on creating several tactics, and some of them require having an optional argument/variable.
I am wondering how to check whether the optional argument was indeed used.
To put everything in context: I want to write a tactic that does the following: takes as “input” an s(intropatterns) and an optional constr input (as t(opt(constr))).
How can we, in this ta...
Discourse Bot (May 21 2021 at 20:52):@AoS posted in Ltac2: pose and exists
Dear community,
I am trying to write an Ltac2 function that combines the pose and the exists functions, as such:
Ltac2 pose_and_exists s t := pose (s := $t); exists $s.This function is supposed to be used in a tactic of the form
Ltac2 Notation "PoseAndExists" s(ident) t(constr) := pose_and_exists s t.However, when testing this tactic on a simple example of the form
Goal exists m: nat, m = ...
Discourse Bot (May 22 2021 at 11:07):@AoS posted in Ltac2: cannot distinguish tactics with same name but different arguments
Dear community,
I was working with Ltac2 on creating some simple tactics, and I ran into the following problem: let us assume that we have some Ltac2 tactics
Ltac2 Notation "Tactic name" s(constr) := ...
Ltac2 Notation "Tactic name" s(constr) "one more word" t(constr) := ...
Discourse Bot (May 30 2021 at 15:09):@AoS posted in Ltac2: timeout tactic
Dear community,
I would like to know if the timeout from Ltac1 tactic still works in Ltac2.
I have tried to use this tactic in Ltac2, but I get the Unbound value timeout error. For instance, the following example works:
Ltac timed_auto := timeout 60 (first [solve [auto] ] ).but the following does not
Ltac2 timed_auto () := timeout 60 (first [solve [auto] ] ).
Discourse Bot (Jun 10 2021 at 13:16):@AoS posted in Ltac2: pose and exists
Dear community,
I would like to create an Ltac2 function that does the equivalent of the following Coq tactics:
pose (ident := constr); exists ident.
An example of the above would be when proving a trivial statement of the form
forall n , exists m, n = m
I know that I can use the pose function from the Ltac2 Std.v file as Std.pose (Some s) t, but I do not know how to continue from here, as `...
Discourse Bot (Jun 10 2021 at 13:32):@AoS posted in Ltac2: unfold
Dear community,
I would like to understand how to use the Ltac2 unfold tactic inside an Ltac2 function.
I know that, when proving a goal, we can use
unfold lemma_name
where lemma_name is the name of a previously proven lemma, and the above tactic unfolds lemma_name in the goal.
However, I would like to create a custom function that calls the Ltac2 unfold tactic. The only way I have managed to...
Discourse Bot (Jun 18 2021 at 20:21):Ignat Insarov @kindaro posted in Standard library of the future?
The problem.
I really want to do computer-assisted proofs. Actually I am looking forward to decades of computer assisted proof writing. But so far it has not been going well. One reason is that libraries are either not there or not accessible.Examples.
This is the official reference for Mathematical Components, the Coq Mathematics standard. Yes, it is an alphabetical index of identifiers. Soun...
Discourse Bot (Jul 16 2021 at 12:25):Théo Zimmermann @Zimmi48 posted in Enforcing that the parser and the documented syntax are in sync
Dear Coq developers and contributors,
We’ve recently merged PR https://github.com/coq/coq/pull/14245.
This PR introduces a new requirement for PR authors, that will be checked in the linter. If your PR modifies the Coq syntax, then you will need to run the make doc_gram_rsts target (as documented in the updated PR template and in coq/README.md at master · coq/coq · GitHub) so that the documented...
Discourse Bot (Aug 24 2021 at 21:18):Liuyinling @lyl posted in Cannot Compile Ynot Library in CoqIDE
I am working on compiling Ynot Library. My idea is just to follow its Tutorial to get a sense of how it turns Coq to be non-terminated and have side effects. Then, I would like to re-implement the certified web services with Ynot. This idea is from the paper called “Certified Web Services in Ynot”.
I have problems compiling the Ynot library. Since this project was created more than ten years ago,...
Discourse Bot (Oct 14 2021 at 10:42):Gaëtan Gilbert @SkySkimmer posted in Coq 8.15 branch date
A branch for Coq 8.15 will be created and enter feature freeze on 2021-11-15.
Pull requests other than bugfixes and documentation updates which are not merged to master before then will not be available in 8.15 barring exceptional circumstances.
If your pull request is blocked by lack of reviewer activity or if you need help to finish it, please push for it in coq calls or on zulip, or risk miss...
Discourse Bot (Dec 07 2021 at 13:52):Gaëtan Gilbert @SkySkimmer posted in Coq 8.15 RC1
The tag for the 8.15 first release candidate has been set (V8.15+rc1).
The 8.15 release will not have any more changes other than bug fixes with low compatibility impact.
Package managers, please start preparing 8.15-compatible versions of your packages.
Discourse Bot (Jan 13 2022 at 16:21):Gaëtan Gilbert @SkySkimmer posted in V8.15.0 tag set
The tag has been set. Opam packages, docker tags and platform versions will now be prepared.
Discourse Bot (Mar 22 2022 at 16:28):Gaëtan Gilbert @SkySkimmer posted in 8.15.1 tagged
The tag for 8.15.1 has been set.
Discourse Bot (Apr 22 2022 at 13:35):Kiran Gopinathan @Gopiandcode posted in Calling Coq from OCaml
I’m working on a project where for various reasons I’ve found myself needing to inspect the intermediate proof contexts of Coq proofs in a programmatic way from OCaml.
Example:
(* proof.v *)Lemma add_comm: forall x y, x + y = y + x.
Proof.
intros x; induction x as [| x IHx].- intros y; induction y; auto.
- intros y.
rewrite plus_Sn_m.
(* [view proof context here] *)
rewrite...
Discourse Bot (Apr 26 2022 at 07:13):Maxime Dénès @maximedenes posted in Coq Working Group June 2022
Hello there,
We had agreed some time ago (during a Coq Call) to hold a two-day Coq Working Group in June, at Inria Sophia-Antipolis. Here’s the evento to pick the date: Répondre au sondage - Coq Working Group June 2022 - Evento
Discourse Bot (May 30 2022 at 08:49):Kiran Gopinathan @Gopiandcode posted in How to evaluate proof terms through opaque definitions?
I was wondering if there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts.
I understand why Coq doesn’t do this by default, and guess it would probably interact in unfavourable ways with proof irrelevance.
My aim is not to use this computation as part of a proof, but rather purely for debugging/meta-analysis - much like how the Print c...
Discourse Bot (May 31 2022 at 11:49):@Gaetan_Gilbert posted in Coq 8.15.2 tagged
The tag for 8.15.2 has been set.
Discourse Bot (Jun 01 2022 at 20:44):@Pierre-Marie_Pedrot (Pierre-Marie Pédrot) posted in Coq 8.16+rc1 has been tagged
Dear package managers,
the V8.16+rc1 tag is now public. Please start preparing the
corresponding packages for the upcoming 8.16.0 release!
Thanks,
PMP
Discourse Bot (Jun 09 2022 at 06:49):@qian posted in rubber tools making
Dear Sir/Madam
Hi, This is qian from Suzhou Kiiwoo Technology Co., Ltd, a Chinese supplier specializing in silicone rubber machinery and molds.
I learned from your company’s website that your company is engaged in the silicone rubber industry, and I hope we can cooperate with you if you have the opportunity.
Our company’s main products are: rubber seals, O-rings, oilfield seals, auto parts, rub...
Discourse Bot (Jul 13 2022 at 14:10):@brando90 posted in How does one access the dependent type unification algorithm from Coq's internals -- especially the one from apply and the substitution solution?
Cross posting because I’ve found that the discussions allows on this cite (that are not usually allowed on stack overflow) can be very useful. So posting:
TLDR: I want to be able to compare two terms – one with a hole and the other without the hole – and extract the actual lambda term that complete the term. Either in Coq or in OCaml or a Coq plugin or in anyway really.
For example, as a toy ex...
Discourse Bot (Jul 14 2022 at 19:20):@brando90 posted in What are Generic Arguments in Coq and how are they structured in their OCaml code?
I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should only be 2 (plus one of the argument seems to skip to other constructors I was expecting based on the OCaml algebraic data type code e.g. OptArg).
I see from coq-serapi:
((GenArg raw (OptArg (ExtraArg ltac_selector)) ())
(GenArg...
Discourse Bot (Sep 05 2022 at 11:56):@ppedrot (Pierre Marie Pédrot) posted in Coq 8.16.0 has been tagged
The V8.16.0 tag is now public!
Package managers should now start work on upgrading their packages.
Discourse Bot (Nov 16 2022 at 17:17):@Zimmi48 (Théo Zimmermann) posted in Branching v8.17 soon
Hello Coq contributors and maintainers,
We are going to create the v8.17 branch in preparation for Coq 8.17 in
the next few days. The tentative schedule can be found here:We have not followed the usual process of announcing the branching
date a month in advance because the choice of release managers has
been made very late. I will be taking this role for this release, with
Gaëtan Gilbert a...
Discourse Bot (Nov 25 2022 at 12:19):@ppedrot (Pierre Marie Pédrot) posted in Coq 8.16.1 has been tagged
The V8.16.1 tag is now public! Package managers should now start work on upgrading their packages.
Discourse Bot (Mar 27 2023 at 06:45):@Zimmi48 (Théo Zimmermann) posted in Coq 8.17.0 tag has been set
Dear Coq developers and maintainers of Coq packages,
The tag for the Coq 8.17.0 release has been set. It is now time to prepare updates to Coq packages.
Thanks!
Théo Zimmermann, release manager for the 8.17 release
Discourse Bot (Mar 29 2023 at 19:57):@carnotweat (sameer gupta) posted in Terms modulo α-conversion and substitution
Can someone explain how ,Coq development does not treat terms modulo α-conversion, therefore the ,substitution a[x ← b] can capture variables. However, it is capture-avoiding if b is
closed, and this suffices to define evaluation and reduction of closed source terms.
From
Discourse Bot (Apr 29 2023 at 02:20):@caverill (Charles Averill) posted in Is there a way to extract ASTs from the Coq compiler?
I’m interested in analyzing the ASTs that the Coq compiler generates while it compiles. Is there any way to extract these by default, or will I have to go digging around in the compiler source?
Last updated: May 31 2023 at 16:01 UTC