The GHC backend sometimes compiles the wrong modules when --interaction is used

[nad]

The GHC backend seems to rely on the current working directory, and this does not work very well when --interaction is used.

Here is one example of what can go wrong:

• Place the following files in the otherwise empty directory A:
  • Main.agda:

    module Main where
    
    import M
    
    main = M.main

  • M.agda:

    module M where
    
    open import Agda.Builtin.IO
    open import Agda.Builtin.String
    open import Agda.Builtin.Unit
    
    postulate
      putStrLn : String → IO ⊤
    
    {-# FOREIGN GHC import qualified Data.Text.IO #-}
    {-# COMPILE GHC putStrLn = Data.Text.IO.putStrLn #-}
    
    main : IO ⊤
    main = putStrLn "A"

• Copy the files to the otherwise empty directory B (placed in the same directory as A), but replace "A" with "B".
• Now invoke Agda in the following way from the directory A:

  printf 'IOTCM "Main.agda" None Indirect (Cmd_compile GHC "Main.agda" [])\nIOTCM "../B/Main.agda" None Indirect (Cmd_compile GHC "../B/Main.agda" [])\n' | agda --interaction --no-libraries
  

  Output:

  Agda2> (agda2-status-action "")
  (agda2-info-action "*Type-checking*" "" nil)
  (agda2-highlight-clear)
  (agda2-info-action "*Type-checking*" "Checking Main ([…]/A/Main.agda).\n" t)
  (agda2-info-action "*Type-checking*" " Checking M ([…]/A/M.agda).\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Primitive in […]/Agda-2.6.3/lib/prim/Agda/Primitive.agdai to […]/A/MAlonzo/Code/Agda/Primitive.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.IO in […]/Agda-2.6.3/lib/prim/Agda/Builtin/IO.agdai to […]/A/MAlonzo/Code/Agda/Builtin/IO.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Bool in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Bool.agdai to […]/A/MAlonzo/Code/Agda/Builtin/Bool.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Maybe in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Maybe.agdai to […]/A/MAlonzo/Code/Agda/Builtin/Maybe.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.List in […]/Agda-2.6.3/lib/prim/Agda/Builtin/List.agdai to […]/A/MAlonzo/Code/Agda/Builtin/List.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Nat in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Nat.agdai to […]/A/MAlonzo/Code/Agda/Builtin/Nat.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Sigma in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Sigma.agdai to […]/A/MAlonzo/Code/Agda/Builtin/Sigma.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Char in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Char.agdai to […]/A/MAlonzo/Code/Agda/Builtin/Char.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.String in […]/Agda-2.6.3/lib/prim/Agda/Builtin/String.agdai to […]/A/MAlonzo/Code/Agda/Builtin/String.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Unit in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Unit.agdai to […]/A/MAlonzo/Code/Agda/Builtin/Unit.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling M in […]/A/M.agdai to […]/A/MAlonzo/Code/M.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Main in […]/A/Main.agdai to […]/A/MAlonzo/Code/Main.hs\n" t)
  (agda2-info-action "*Type-checking*" "Calling: ghc -O -o […]/A/Main -Werror -i[…]/A -main-is MAlonzo.Code.Main […]/A/MAlonzo/Code/Main.hs --make -fwarn-incomplete-patterns\n" t)
  (agda2-info-action "*Type-checking*" "[1 of 7] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )\n" t)
  (agda2-info-action "*Type-checking*" "[2 of 7] Compiling MAlonzo.Code.Agda.Builtin.Unit ( MAlonzo/Code/Agda/Builtin/Unit.hs, MAlonzo/Code/Agda/Builtin/Unit.o )\n" t)
  (agda2-info-action "*Type-checking*" "[3 of 7] Compiling MAlonzo.Code.Agda.Builtin.String ( MAlonzo/Code/Agda/Builtin/String.hs, MAlonzo/Code/Agda/Builtin/String.o )\n" t)
  (agda2-info-action "*Type-checking*" "[4 of 7] Compiling MAlonzo.Code.Agda.Builtin.IO ( MAlonzo/Code/Agda/Builtin/IO.hs, MAlonzo/Code/Agda/Builtin/IO.o )\n" t)
  (agda2-info-action "*Type-checking*" "[5 of 7] Compiling MAlonzo.Code.M   ( MAlonzo/Code/M.hs, MAlonzo/Code/M.o )\n" t)
  (agda2-info-action "*Type-checking*" "[6 of 7] Compiling MAlonzo.Code.Main ( […]/A/MAlonzo/Code/Main.hs, […]/A/MAlonzo/Code/Main.o )\n" t)
  (agda2-info-action "*Type-checking*" "[7 of 7] Linking […]/A/Main\n" t)
  (agda2-status-action "Checked")
  (agda2-info-action "*Compilation result*" "The module was successfully compiled with backend GHC.\n" nil)
  ((last . 1) . (agda2-goals-action '()))
  Agda2> (agda2-status-action "")
  (agda2-info-action "*Type-checking*" "" nil)
  (agda2-highlight-clear)
  (agda2-info-action "*Type-checking*" "Checking Main ([…]/B/Main.agda).\n" t)
  (agda2-info-action "*Type-checking*" " Checking M ([…]/B/M.agda).\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Primitive in […]/Agda-2.6.3/lib/prim/Agda/Primitive.agdai to […]/B/MAlonzo/Code/Agda/Primitive.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.IO in […]/Agda-2.6.3/lib/prim/Agda/Builtin/IO.agdai to […]/B/MAlonzo/Code/Agda/Builtin/IO.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Bool in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Bool.agdai to […]/B/MAlonzo/Code/Agda/Builtin/Bool.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Maybe in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Maybe.agdai to […]/B/MAlonzo/Code/Agda/Builtin/Maybe.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.List in […]/Agda-2.6.3/lib/prim/Agda/Builtin/List.agdai to […]/B/MAlonzo/Code/Agda/Builtin/List.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Nat in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Nat.agdai to […]/B/MAlonzo/Code/Agda/Builtin/Nat.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Sigma in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Sigma.agdai to […]/B/MAlonzo/Code/Agda/Builtin/Sigma.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Char in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Char.agdai to […]/B/MAlonzo/Code/Agda/Builtin/Char.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.String in […]/Agda-2.6.3/lib/prim/Agda/Builtin/String.agdai to […]/B/MAlonzo/Code/Agda/Builtin/String.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Agda.Builtin.Unit in […]/Agda-2.6.3/lib/prim/Agda/Builtin/Unit.agdai to […]/B/MAlonzo/Code/Agda/Builtin/Unit.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling M in […]/B/M.agdai to […]/B/MAlonzo/Code/M.hs\n" t)
  (agda2-info-action "*Type-checking*" "Compiling Main in […]/B/Main.agdai to […]/B/MAlonzo/Code/Main.hs\n" t)
  (agda2-info-action "*Type-checking*" "Calling: ghc -O -o […]/B/Main -Werror -i[…]/B -main-is MAlonzo.Code.Main […]/B/MAlonzo/Code/Main.hs --make -fwarn-incomplete-patterns\n" t)
  (agda2-info-action "*Type-checking*" "[6 of 7] Compiling MAlonzo.Code.Main ( […]/B/MAlonzo/Code/Main.hs, […]/B/MAlonzo/Code/Main.o )\n" t)
  (agda2-info-action "*Type-checking*" "[7 of 7] Linking […]/B/Main\n" t)
  (agda2-status-action "Checked")
  (agda2-info-action "*Compilation result*" "The module was successfully compiled with backend GHC.\n" nil)
  ((last . 1) . (agda2-goals-action '()))
  Agda2> 
  

  Note that GHC only compiled one module from B.
• Let's now run A/Main and B/Main:

  $ A/Main
  A
  $ B/Main
  A
  

  The program B/Main should print B, not A.

I don't know if the JS backend is affected by a similar problem.

[nad]

Perhaps this can be fixed by invoking GHC from a specific directory.

[nad]

If Agda is invoked from the command-line, and the user gives the option --ghc-flag=-idir, then it may be confusing if dir is not interpreted relative to the current working directory. Thus I decided to invoke GHC from the directory containing the MAlonzo directory when --interaction or --interaction-json is used, and to use the current working directory otherwise.