TODO.

42e700e9 · POTTIER Francois · 10793049 · 42e700e9 · 42e700e9
Commit 42e700e9 authored Apr 06, 2017 by POTTIER Francois
Hide whitespace changes
Inline Side-by-side

Showing with 8 additions and 3 deletions

TODO TODO +0 -3

TODO-NOT! TODO-NOT! +8 -0

No files found.
--- a/TODO
+++ b/TODO
@@ -27,9 +27,6 @@
  - Change of LICENSE. Clarify the status of test/.
  - Send CompCert pull request.

-* The table back-end should not use Invariant at all?
-  And we should be able to save time by not running Invariant.
-
 * Move more of ErrorReports from CompCert to MenhirLib.
  In [show], might want to apply [shorten] to the output of [f].


--- a/TODO-NOT!
+++ b/TODO-NOT!
@@ -73,3 +73,11 @@ for now.
  an associativity status (%left, %right, %nonassoc) one should be allowed
  to declare %neutral and obtain an unspecified associativity status
  (causing an error if this status is ever consulted).
+
+* Since the table back-end does not use the module Invariant,
+  it should be possible to save time, in --table mode,
+  by not running the analysis in Invariant.
+  That would require making Invariant a functor,
+  and calling it inside CodeBackend, CoqBackend, and Interpret (complicated).
+  Or perhaps just running the computation on demand (using lazy)
+  but that makes timing more difficult.