Here is a link for discussing issues and plans about the architecture of `declare.ml`

(to fill by Monday evening):

https://evento.renater.fr/survey/discussion-on-declare-ml-4my4j4hn

Questions involved are:

- treatment of side effects (schemes, abstract, ...) in proof/obligation mode (queueing them to the sigma until completion of the interactive constant?)
- emulating the obligation mode on top of the proof mode?
- further simplification of
`declare.ml`

: reducing the 6 different paths for (direct | proof-based | obligation-based) ⨯ (single | mutual) to only 1 execution path? - a policy for universes (when to restrict, minimize, hide universes of opaque bodies), consistent over the different declarations?
- supporting
`wf`

/`measure`

even without`Program`

/`Function`

; supporting`Theorem with`

/`Definition`

with partial subterms even without`Program`

; which policy on evars not resolved by unification or type classes (application of an inference hook, failure, obligation), and on which kinds of evars? - CEP #42
- UI requirements

One could typically plan to have 2-4 meetings on the topic, each one organized around a 10-20 minutes talk, built on a few slides, followed by a discussion (who would be willing to give a talk?)

Cc: @Pierre-Marie Pédrot, @Emilio Jesús Gallego Arias, @Matthieu Sozeau, @Andres Erbsen, ...

are these really related to `declare.ml`

?

- supporting
`wf`

/`measure`

even without`Program`

/`Function`

; supporting`Theorem with`

/`Definition`

with partial subterms even without`Program`

; which policy on evars not resolved by unification or type classes (application of an inference hook, failure, obligation), and on which kinds of evars? - CEP #42

are these really related to

`declare.ml`

?

Right, they rather correspond to choices made in `vernacentries.ml`

, `comFixpoint`

and `comDefinition.ml`

on how they connect to the `declare.ml`

API (see PR #18811) but I'd be interested to have them part of the discussion though.

PS: The cc list correspond to the names I noted from the last call (and maybe did I miss names). If posted here, it is of course that it is neither limited to these names, nor to the persons present at last call.

Another case where definition creation and evars interact is `Derive`

, where proof mode is entered once but two definitions are created. IIRC another, seemingly orthogonal, feature of `Derive`

is that it allows proof mode to be entered without first resolving all evars in the type of the lemma. I don't know how it works under the hood, but in terms of capability it might actually as powerful as some hypothetical combinations of other modes mentioned.

Up to now, next Thursday 4pm seems to be a good date. I'll give a short presentation (mostly on my experience with factorizing executation paths and on what to possibly do next). @Emilio Jesús Gallego Arias, @Pierre-Marie Pédrot, @Gaëtan Gilbert , @Pierre Roux, ... will you be able to attend?

I'm away on vacations most of the next two weeks

Ah, but you mean this Thursday 18th? I can be around then.

Another case where definition creation and evars interact is

`Derive`

.

I did not know that `Derive`

was used in the large. Morally, it could be seen as a generalization of `Theorem with`

with dependent statements (though not dependent proofs).

```
Theorem prop_of_id : P id
with id : T.
```

It would be easy (and natural) to integrate it to the general scheme.

I don't know how it works under the hood

Iiuc, it relies on a (single) ordinary proof state (i.e. one evar map, one structure of focus, etc.) but two (or virtually more in the code) final targets.

Actually, iirc, Matthieu's inductive-inductive branch includes dependent mutual fixpoints, that is statements like:

```
Fixpoint f1 : T1
with f2 : T2(f1)
...
with fn : Tn(f1, ..., f_{n-1}).
```

So, if we accept this general syntax, `Derive`

is a particular case without mutual recursion.

Yep, Derive is ubiquitous in Rupicola (even appears in the paper) and Fiat-Crypto and would probably have been very useful for other Fiat-* projects if we had known about it earlier. For a previously disused plugin, it has held up impressively well. The generalization you suggest seems good.

Tomorrow at 4pm works for me Hugo

@Hugo Herbelin where do we meet?

same question ?

We can use our usual room?

https://rendez-vous.renater.fr/coq-call ?

fine by me

Ok

Abusing derive for lemma with evars in statement:

```
Require Import Derive.
Derive __unused_name SuchThat (3 = _) As mylemma.
Proof. exact eq_refl.
Unshelve. exact True. exact I. Defined.
```

A late partial summary of the call on declare.ml:

- Emilio mentions the Proof Handling Refactoring PRs (summarizing issue 10041 and related Coq project)
- About deprecation of
`Function`

, general agreement (including Andres) - A priori, agreement on giving autonomous access to the different parts of Program (like
`Set Program Cases`

, but also autonomous access to the use of the program inference hook, to the obligation mechanism, to the`measure`

/`wf`

specific`Program`

-encapsulation) - Matthieu not opposed to move Equations to the Coq archive
- A priori ok to rethink at obligations on top of the proof engine
- PMP suggests that evars of kinds that have a semantic role and are not already in a table are registered in a table (next to
`obligation_evars`

in`Evd.evar_flags`

)

(Please report lacks or inaccuracies)

Last updated: Oct 13 2024 at 01:02 UTC