[Ltac2] Add util files for Bool, List, Option #10219

JasonGross · 2019-05-22T21:23:08Z

Most functions are taken either from the Coq standard library or the
OCaml standard library. One (enumerate) is taken from Python. Most
names are chosen according to OCaml conventions (as Coq does not have
exceptions, and so the OCaml naming conventions already distinguish
between option and exception). Since exists is a keyword, we use the
Coq name existsb instead. We generally favor Coq argument ordering
when there is a conflict between Coq and OCaml.

Note that seq matches neither Coq nor OCaml; it takes a step
argument for how much to increment by on each step.

Sorting functions are mostly taken from Coq's mergesort library; it
might make sense to replace them with OCaml's versions for efficiency?

Kind: feature.

Fixes / closes coq/ltac2#19 (mostly; I haven't ported the reimplementation of lazy_match, but I think that's okay)

Which of these should this PR get?

Added / updated test-suite

Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

ppedrot · 2019-05-22T21:27:26Z

user-contrib/Ltac2/List.v

+
+Ltac2 hd (ls : 'a list) :=
+  match ls with
+  | [] => Control.zero (Tactic_failure (Some (Message.of_string "hd")))


This needs to be discussed in the API guidelines, but I don't think using backtracking exceptions for anything else than proof search is a good idea. I believe that instead panics should be used when preconditions of a function call are not satisfied, which looks like this is the case here.

I think there are three sorts of errors, and it is important to be able to express all of them:

Control.zero - failure in the tactic monad. I agree that this is the wrong type of failure for this method.

Catchable exceptions. I think the only catchable exceptions are currently the ones that induce backtracking,* which I think is wrong.

Anomalies (or uncatchable exceptions)

See, for example, #10094 and #10095, where the inability to catch an exception makes it significantly harder to implement a thing.

If you make a version of Control.case that can catch exceptions raised by Control.throw (or else a version of Control.throw whose exceptions can be caught by Control.case), then I'm happy to replace all of the Control.zeros here with Control.throw.
* For example:
Require Import Ltac2.Init. Require Ltac2.Control. Require Ltac2.Message. Goal True. match Control.case (fun _ => Control.throw Not_found) with | Val a => () | Err e => Message.print (Message.of_exn e) end. (* Error: Uncaught Ltac2 exception: Not_found *)

My take on that is that we should not reenact the exception hell of OCaml, and separate potential failure from invariant breakage via types. That is, a function that might rightfully "fail" should return options, while a function whose preconditions are violated should return a panic. In OCaml there is a pervasive confusion between these two situations, which leads to catastrophic semantics when trying to scale. (Anomaly: Uncaught exception Not_found might be the single most frequent anomaly raised by Coq for instance.)

There is nothing complicated in doing so, it's just a matter of sticking to a particular style. For instance, your examples could be given as pairs of functions, one to check you are in the right fragment, and one to extract the relevant date assuming the first one says it's OK.

In the case of this PR, hd should fail with a panic. It's your duty to ensure that the list is not empty beforehand, and if you don't know, then just use pattern-matching.

Zimmi48 · 2019-05-22T22:05:56Z

user-contrib/Ltac2/Bool.v

+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)


This is an outdated header. I wonder where you found it. OMG you found it in the code of Ltac2! I wonder how I could let that split. Anyway, you can find the right header in dev/header.ml

Is dev/header.ml supposed to only extend to 2018, not 2019?

In any case, I've updated the headers of the new files I added

We didn't update any header since 2019 😢 But yes, it is supposed to extend.

Note that there is #10320 now, so you could adapt this PR accordingly.

Most functions are taken either from the Coq standard library or the OCaml standard library. One (`enumerate`) is taken from Python. Most names are chosen according to OCaml conventions (as Coq does not have exceptions, and so the OCaml naming conventions already distinguish between option and exception). Since `exists` is a keyword, we use the Coq name `existsb` instead. We generally favor Coq argument ordering when there is a conflict between Coq and OCaml. Note that `seq` matches neither Coq nor OCaml; it takes a `step` argument for how much to increment by on each step. Sorting functions are mostly taken from Coq's mergesort library; it might make sense to replace them with OCaml's versions for efficiency?

SkySkimmer · 2019-06-06T15:55:03Z

user-contrib/Ltac2/Option.v

+
+Ltac2 ret (x : 'a) := Some x.
+
+Ltac2 lift (f : 'a -> 'b) (x : 'a option) := map f x.


What's the point of this alias?

I would say the name lift is more common when it is partially applied to lift f to 'a option -> 'b option. The name map is more common when it is fully applied. I am usually not a fan of aliases but would say it makes sense in this case because it is more a coincidence that lift and map have the same implementation.

MSoegtropIMC · 2019-06-07T09:58:36Z

user-contrib/Ltac2/Int.v

+Ltac2 gt (x : int) (y : int) := equal (compare x y) 1.
+Ltac2 le (x : int) (y : int) :=
+  (* we might use [lt x (add y 1)], but that has the wrong behavior on MAX_INT *)
+  match equal x y with


Wouldn't it be more efficient to match on "compare x y" here?

Please ignore, I just learned myself that matching on integers is not yet supported in Ltac2.

MSoegtropIMC · 2019-06-13T15:58:07Z

@JasonGross: do you agree that most (or probably all) of the Control.zero should be replaced with Control.throw? I agree with @ppedrot that for things like an out of bounds access, a non backtrackable throw would probably help with debugging and getting things right. Also you supply option variants e.g. for hd in case one is not sure. In case you are busy right now, I could also propose a patch for your PR.

@ppedrot : are there any other points which keep this PR from merging? It is a bit hard to work with Ltac2 if basic stuff as defined here is missing.

JasonGross · 2019-06-13T19:32:39Z

I am pretty busy, please do propose a patch and I will merge. I am mostly sold by the reasoning ppedrot gave, and certainly sold enough to replace all the zeros with throws in this PR

… out of courtesy) - index errors (negative or out of bounds) generally throw (panic) - hd, last, find backtrack, because here backtracking can actually be useful added a _throw variant to these functions which panics This emaphasizes the difference between backtracking and throwing exceptions, which doesn't exist in OCaml. - simplified the implementation of for_all2 and exist2 (ok, that is a matter of taste ...) - added assertions which combine a boolean match with a throw. This makes the code more readable and makes it easier to have more specific error messages. - added a lastn function - gave Out_of_bounds a message argument (there is no good reason why invalid_argument has one and this not) All other exceptions without message argument are quite specific to certain functions (like Not_Found)

MSoegtropIMC · 2019-06-16T07:59:26Z

@JasonGross : I took the freedom to directly push to your PR branch. This makes it easier for others to review my changes in parallel. See the commit message for the changes I did. I hope this is agreeable.

Note on Bool: I find it questionable to use the "b" extension since in Ltac2 there is no differentiation between Prop and bool. I would rather remove this (but didn't do so). The syntax is more like OCaml than like Coq so I would stick to names one would have chosen in OCaml (if these functions wouldn't be operators).

In list I removed the "b" aliases to various exist and for_all functions.

MSoegtropIMC · 2019-06-17T16:34:16Z

@JasonGross : I take your 👍 as agreement to remove the "b" extensions in Bool.v. I think this would lead to a more regular naming since e.g. the comparison function in Int.v also don't have a "b". I will do this a separate commit.

Changed year in headers

MSoegtropIMC · 2019-06-19T08:48:42Z

@ppedrot : would it be possible to merge this PR and later also my PRs (which depend on this)? In my view Ltac2 is very important for Coq and a standard library is very important for Ltac2. We shouldn't stall the good momentum we have right now.

I find @JasonGross approach to follow the API of the OCaml library very agreeable, because it will make it easier to port Ltac-2 to OCaml.

ppedrot

I don't agree with the current scheme for failure handling. We should have only two variants, not four.

A version that uses throw, with the default name (e.g. hd)
A version that returns option, with the _opt suffix

Exporting backtrack in standard functions not meant for proof search is another recipe for explosive disaster (in particular as the default function), and default values contaminate the API.

ppedrot · 2019-06-19T09:00:34Z

@MSoegtropIMC Instead, you should provide option combinators that turn them into backtracking failures and default values accordingly.

MSoegtropIMC · 2019-06-19T09:45:27Z

@ppedrot : I agree with your comment - less functions and explicit backtracking with an option combinator will most likely help the user the get what (s)he wants. I think my Array.v PR already follows your advice (for array index bound errors it anyway makes no sense to backtrack) but I will review it again with this in mind.

@JasonGross : I will follow @ppedrot advice and reduce the number of options and add the combinators he suggested to Option.v. I hope you agree with this as well.

MSoegtropIMC · 2019-06-19T09:54:46Z

user-contrib/Ltac2/List.v

+  | Some v => v
+  | None => Control.zero Not_found
+  end.
+


@ppedrot : I assume your comment also applies to find above. Here I could imagine that a backtracking Control.zero Not_found might sometimes be what people want, but I guess it is better to make the backtracking always explicit in this kind of library function. Unless I hear from you otherwise, I will change this as well.

…ded option combinators

ppedrot · 2019-06-25T14:33:56Z

@MSoegtropIMC sorry for the late review, the request somewhat flew under my radar.

Ack-by: JasonGross Ack-by: MSoegtropIMC Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ppedrot

MSoegtropIMC · 2019-07-25T06:44:54Z

@vbgl : would you mind merging this into 8.10? Ltac2 is unusable without such a mini library. The bad thing is that people would start to develop their own incompatible libraries and distribute them.

MSoegtropIMC · 2019-07-25T06:49:08Z

@vbgl: I just saw that 8.10 has still separate ltac2, so this would get a bit tricky. If you want me to prepare a PR, please let me know.

vbgl · 2019-07-25T07:49:15Z

There is no Ltac2 in 8.10 and the legacy repository for Ltac2 has been frozen. So I don’t understand any of your requests. Sorry.

MSoegtropIMC · 2019-07-25T07:54:24Z

Yes, indeed it would get tricky. Well it is not that bad - since this PR didn't change anything on the ML side people can use the latest Ltac2 .v files and recompile them on their own (that's what I am doing when working with 8.10).

Zimmi48 · 2019-07-25T08:01:52Z

FTR the reason the Ltac2 repository has been frozen is that his author won't maintain it, especially given that most changes to the ML side would require the corresponding changes in Coq's API. However, nothing would prevent us from unfreezing the repository, and let a developer (if one volunteers to do it) backport to v8.10 any Ltac2 change that can be (such as these library files), and then prepare a release.

MSoegtropIMC · 2019-07-25T08:50:52Z

@Zimmi48 : I would be open to do that if @vbgl as release manager agrees that it makes sense. I think Ltac-2 is an important development which deserves some acceleration.

You know my opinion on Ltac-1: Ltac-1

vbgl · 2019-07-25T09:18:24Z

Ltac-2 is already in the CI for the 8.10 branch. If Michael volunteers to maintain the https://github.com/coq/ltac2 repository, it does make sense to unfreeze it, backport valuable contributions and make Ltac-2 for Coq 8.10 a useful plug-in.

MSoegtropIMC · 2019-07-25T09:21:20Z

@vbgl : what is your time line for the 8.10 release?

Zimmi48 · 2019-07-25T09:22:41Z

@MSoegtropIMC I have now unfrozen the repository and made you a collaborator. Note that even in the event that you were late for the 8.10.0 release, it would still make sense to update the v8.10 branch of Ltac2, produce a new release, and include it in the 8.10.1 Windows installer, so I would say no rush.

MSoegtropIMC · 2019-07-25T09:34:34Z

@Zimmi48 : thanks! I will do a back port for 8.10 then.

JasonGross added part: standard library The standard library stdlib. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. labels May 22, 2019

JasonGross added this to the 8.11+beta1 milestone May 22, 2019

JasonGross requested review from Zimmi48 and ppedrot May 22, 2019 21:23

ppedrot reviewed May 22, 2019

View reviewed changes

Zimmi48 reviewed May 22, 2019

View reviewed changes

JasonGross force-pushed the ltac2-list-bool-util branch from 580dc42 to cd6db46 Compare May 23, 2019 01:15

Zimmi48 mentioned this pull request May 31, 2019

Add Bool and List util functions coq/ltac2#19

Closed

SkySkimmer reviewed Jun 6, 2019

View reviewed changes

MSoegtropIMC reviewed Jun 7, 2019

View reviewed changes

This was referenced Jun 7, 2019

Anomaly in Ltac2 #10339

Closed

Resolve 10342 : [Ltac2] Add array library #10343

Merged

Removed "b" from function names in Bool.v

01d0b60

Changed year in headers

ppedrot requested changes Jun 19, 2019

View reviewed changes

MSoegtropIMC reviewed Jun 19, 2019

View reviewed changes

Removed backtracking and default variants of various functions and ad…

8137e40

…ded option combinators

MSoegtropIMC requested a review from ppedrot June 19, 2019 11:14

ppedrot approved these changes Jun 25, 2019

View reviewed changes

ppedrot self-assigned this Jun 25, 2019

ppedrot merged commit 8137e40 into coq:master Jun 25, 2019

ppedrot added a commit that referenced this pull request Jun 25, 2019

Merge PR #10219: [Ltac2] Add util files for Bool, List, Option

7024688

Ack-by: JasonGross Ack-by: MSoegtropIMC Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ppedrot

MSoegtropIMC added a commit to MSoegtropIMC/coq that referenced this pull request Jun 26, 2019

Adjusted Ltac2 system functions to PR coq#10219

566f226

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Ltac2] Add util files for Bool, List, Option #10219

[Ltac2] Add util files for Bool, List, Option #10219

JasonGross commented May 22, 2019

ppedrot May 22, 2019

JasonGross May 23, 2019 •

edited

ppedrot Jun 8, 2019

Zimmi48 May 22, 2019

JasonGross May 23, 2019

JasonGross May 23, 2019

Zimmi48 May 23, 2019

Zimmi48 Jun 17, 2019

SkySkimmer Jun 6, 2019

MSoegtropIMC Jun 16, 2019

MSoegtropIMC Jun 7, 2019

MSoegtropIMC Jun 8, 2019

MSoegtropIMC commented Jun 13, 2019

JasonGross commented Jun 13, 2019

MSoegtropIMC commented Jun 16, 2019

MSoegtropIMC commented Jun 17, 2019

MSoegtropIMC commented Jun 19, 2019

ppedrot left a comment

ppedrot commented Jun 19, 2019

MSoegtropIMC commented Jun 19, 2019

MSoegtropIMC Jun 19, 2019

ppedrot commented Jun 25, 2019

MSoegtropIMC commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019

vbgl commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019

Zimmi48 commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019

vbgl commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019

Zimmi48 commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019


		Ltac2 ret (x : 'a) := Some x.

		Ltac2 lift (f : 'a -> 'b) (x : 'a option) := map f x.

[Ltac2] Add util files for Bool, List, Option #10219

[Ltac2] Add util files for Bool, List, Option #10219

Conversation

JasonGross commented May 22, 2019

Choose a reason for hiding this comment

JasonGross May 23, 2019 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MSoegtropIMC commented Jun 13, 2019

JasonGross commented Jun 13, 2019

MSoegtropIMC commented Jun 16, 2019

MSoegtropIMC commented Jun 17, 2019

MSoegtropIMC commented Jun 19, 2019

ppedrot left a comment

Choose a reason for hiding this comment

ppedrot commented Jun 19, 2019

MSoegtropIMC commented Jun 19, 2019

Choose a reason for hiding this comment

ppedrot commented Jun 25, 2019

MSoegtropIMC commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019

vbgl commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019

Zimmi48 commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019

vbgl commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019

Zimmi48 commented Jul 25, 2019

MSoegtropIMC commented Jul 25, 2019

JasonGross May 23, 2019 •

edited