Incremental compilation produces bad executables when missing incremental compile data

[Z-snails]

If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!

Steps to Reproduce

https://gist.github.com/Z-snails/33bda6b1764d8d601a7680c8ccaa3e2a run sh build.sh

Expected Behavior

prints "hello world"

Observed Behavior

Exception: variable Mod2-main is not bound

Either idris should give an error while compiling or return to whole program compilation

[iacore]

The problem is that Idris refuse compile the module again in incremental mode if it finds the same module already compiled in "whole program mode".

In "whole program mode", Idris still produce 1 TTC per .idr file. It should be possible to continue from there to get incremental chez file *.so .

[dunhamsteve]

I could see cases where there is both a .ttc and a .so, but the .so is older than the .ttc (e.g. compile with incr on, change file, compile with incr off, then compile with incr on again). It might be necessary to check that the .so is both present and up to date when deciding whether to rebuild the module or use the existing ttc.

[dunhamsteve]

Interesting. So the .ttc file says if there is a .so or not. And it collects that information to know what to link, but doesn't actually include the code in the non .so case. So if there is a Mod1.so sitting on disk and the latest Mod1.ttc says it's not incremental, it won't link the stale .so, but also neglects to include the code from the .ttc.

[dunhamsteve]

Ok, it was more subtle than I thought, but it looks like this will fix the issue. The root cause is that Idris will drop the allIncData for a backend if the data is missing for that backend in one of the ttc files, but when processing a subsequent file it recreates a record for that backend.

Above, I was thinking that you could just rebuild the .ttc/.so, but hadn't considered the case of installed libraries. There is a lot of code already in case to handle missing incremental data by switching to whole program.

One possible future improvement would be to take a hybrid approach and do best effort incremental - use the available incremental parts and whole program the rest.

diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index f40285eb..659a384c 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -2474,6 +2474,10 @@ addImportedInc modNS inc
                   do recordWarning (GenericWarn ("No incremental compile data for " ++ show modNS))
                      defs <- get Ctxt
                      put Ctxt ({ allIncData $= drop cg } defs)
+                     -- The cg dropped from allIncData is re-added below
+                     case show modNS of
+                        "" => pure ()
+                        _  => updateSession { incrementalCGs $= (delete cg) }
                 Just (mods, extra) =>
                      put Ctxt ({ allIncData $= addMod cg (mods, extra) }
                                       defs)