Stream: Coq devs & plugin devs

Topic: Abort for modules/program?

Gaëtan Gilbert (Nov 12 2021 at 13:22):

I feel like there was a way to give up on obligations but can't remember the command.
AFAIK there is no way to give up on an open module, not sure if it would be useful (typically it would be used for a test like

Module M : T.
(* stuff *)
Fail End M.
Giveup M.

)

Théo Zimmermann (Nov 12 2021 at 13:36):

It could also be useful for teaching material (if you don't want to save what you did in a "failed attempt" module.

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:14):

I'm not sure the mess with the document structure (*) is worth the gain here. This kind of tests could be done better with using a different interface that is not the document, but something which understands document operations.

(*) think of tools such as editors etc... get much more complex once you have such non-structural stuff

Gaëtan Gilbert (Nov 12 2021 at 14:17):

I don't get it

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:19):

What you don't get?

Gaëtan Gilbert (Nov 12 2021 at 14:20):

what mess is there?

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:20):

What I don't like is to give stuff such as Module M. .... End M. a sequential interpretation

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:20):

The mess is that I can't see my document as something where Module of mod_data * cmds is a constructor

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:21):

now modules become global state transformers

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:21):

so the tradeoff for me is not enough

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:21):

as for a start, using what are supposed to be Coq documents to script tests seems wrong

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:21):

we had a pretty interesting discussion about this the other day tho, for example how people work on Jupyter vs the way you work on Coq

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:23):

But that's a subjective view, of course

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:23):

Note that for example, the way I handle this stuff in the current version of my doc manager is that implicitly close every open struct

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:23):

so I keep the "parenthesization"

Théo Zimmermann (Nov 12 2021 at 14:23):

cc @Jason Gross (who could also be interested in such a feature...)

Emilio Jesús Gallego Arias (Nov 12 2021 at 14:24):

so if the user writes module M ... Bar. and doesn't close it, all the tools see and End M. at the end.

Last updated: Sep 09 2024 at 05:02 UTC