diff options
| -rw-r--r-- | doc/changelog/04-tactics/14012-ltac2-array-init.rst | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_14011.v | 23 | ||||
| -rw-r--r-- | user-contrib/Ltac2/Array.v | 2 |
3 files changed, 28 insertions, 1 deletions
diff --git a/doc/changelog/04-tactics/14012-ltac2-array-init.rst b/doc/changelog/04-tactics/14012-ltac2-array-init.rst new file mode 100644 index 0000000000..c79fc7e29a --- /dev/null +++ b/doc/changelog/04-tactics/14012-ltac2-array-init.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Ltac2 ``Array.init`` no longer incurs exponential overhead when used + recursively (`#14012 <https://github.com/coq/coq/pull/14012>`_, fixes `#14011 + <https://github.com/coq/coq/issues/14011>`_, by Jason Gross). diff --git a/test-suite/bugs/closed/bug_14011.v b/test-suite/bugs/closed/bug_14011.v new file mode 100644 index 0000000000..c1d3ce7a89 --- /dev/null +++ b/test-suite/bugs/closed/bug_14011.v @@ -0,0 +1,23 @@ +(** Test that Ltac2 Array.init doesn't compute the first argument twice, and has the correct asymptotics when nested *) +Require Import Ltac2.Ltac2. +Ltac2 Type rec singleton := [ Single (int) | Arr (singleton array) ]. +Ltac2 rec init_rec (n : int) := + match Int.equal n 0 with + | true => Single 0 + | false => Arr (Array.init 1 (fun _ => init_rec (Int.sub n 1))) + end. +Ltac2 rec timing (n : int) := + (match Int.equal n 0 with + | true => () + | false => timing (Int.sub n 1) + end; + Message.print (Message.concat (Message.of_int n) (Message.of_string ": ")); + let _ := Control.time None (fun _ => init_rec n) in + ()). +(** Should take less than 0.1 seconds if the asymptotics are correct. +Previous behavior was to take an expected 1 million times the age of +the universe. Capping the time at 100 seconds seems like a reasonable +middle ground between these times, as I expect that compilation of Coq +itself will not finish in reasonable time if the computer is running +1000x slower than modern machines. *) +Timeout 100 Ltac2 Eval timing 100. diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v index 5adba829c5..b5e7f37c9f 100644 --- a/user-contrib/Ltac2/Array.v +++ b/user-contrib/Ltac2/Array.v @@ -70,7 +70,7 @@ Ltac2 init (l : int) (f : int->'a) := | true => empty () | false => let arr:=make l (f 0) in - init_aux arr 0 (length arr) f; + init_aux arr 1 (Int.sub l 1) f; arr end. |