**Ł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...

(The above is not really "new" but a test that the Discourse integration correctly works.)

**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?

**@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...

**@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?

**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

**@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?

**@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.

**@randair** posted in **Proofview.tactic to string or Pp.t**

Is there a way to print a Proofview.tactic as an Ltac expression?

**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 ...

**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)...

**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,

**@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...

**@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...

**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

**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...

**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...

**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 ...

**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...

**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 ...

**@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...

**@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...

**@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 = ...

**@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) := ...

**@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] ] ).

**@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 `...

**@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...

**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...

**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...

**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,...

**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...

**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.

**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.

**Gaëtan Gilbert @SkySkimmer** posted in **8.15.1 tagged**

The tag for 8.15.1 has been set.

**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...

**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

**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...

**@Gaetan_Gilbert** posted in **Coq 8.15.2 tagged**

The tag for 8.15.2 has been set.

**@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

**@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...

**@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...

**@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...

**@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.

**@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...

**@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.

**@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

**@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

**@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