Stream: Coq devs & plugin devs

Topic: New Discourse topics


view this post on Zulip 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...

view this post on Zulip Théo Zimmermann (Jun 18 2020 at 16:50):

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

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 ...

view this post on Zulip 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)...

view this post on Zulip 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,

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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 ...

view this post on Zulip 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...

view this post on Zulip 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 ...

view this post on Zulip 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 Type

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

view this post on Zulip 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...

view this post on Zulip 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 = ...

view this post on Zulip 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) := ...

view this post on Zulip 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] ] ).

view this post on Zulip 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 `...

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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,...

view this post on Zulip 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...


Last updated: Oct 16 2021 at 07:02 UTC