Stream: Coq devs & plugin devs

Topic: Abort for modules/program?


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

)

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

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

view this post on Zulip Gaëtan Gilbert (Nov 12 2021 at 14:17):

I don't get it

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 14:19):

What you don't get?

view this post on Zulip Gaëtan Gilbert (Nov 12 2021 at 14:20):

what mess is there?

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 14:21):

now modules become global state transformers

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 14:21):

so the tradeoff for me is not enough

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 14:23):

But that's a subjective view, of course

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 14:23):

so I keep the "parenthesization"

view this post on Zulip Théo Zimmermann (Nov 12 2021 at 14:23):

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

view this post on Zulip 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: Feb 05 2023 at 19:29 UTC