Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
nad opened this issue Oct 15, 2022 · 2 comments
Closed

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

nad opened this issue Oct 15, 2022 · 2 comments
Assignees
@nad
Labels
backend: ghc Haskell code generation backend ("MAlonzo") documented-in-changelog Issues already documented in the CHANGELOG type: bug Issues and pull requests about actual bugs
Milestone
2.6.3

Comments

@nad
Copy link
Contributor

nad commented Oct 15, 2022

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 nad added type: bug Issues and pull requests about actual bugs backend: ghc Haskell code generation backend ("MAlonzo") labels Oct 15, 2022
@nad nad added this to the 2.6.4 milestone Oct 15, 2022
@nad
Copy link
Contributor Author

nad commented Oct 15, 2022

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

@nad nad self-assigned this Oct 24, 2022
@nad nad modified the milestones: 2.6.4, 2.6.3 Oct 24, 2022
nad added a commit that referenced this issue Oct 24, 2022
@nad
[ #6194 ] Added a working directory argument to callCompiler.
d89a2ec
nad added a commit that referenced this issue Oct 24, 2022
@nad
Fixed #6194.
8790675
@nad nad mentioned this issue Oct 24, 2022
Merged
nad added a commit that referenced this issue Oct 24, 2022
@nad
[ #6194 ] Added a working directory argument to callCompiler.
f9a8ac1
nad added a commit that referenced this issue Oct 24, 2022
@nad
Fixed #6194.
a442bfa
@nad
Copy link
Contributor Author

nad commented Oct 24, 2022

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.

nad added a commit that referenced this issue Oct 25, 2022
@nad
[ #6194 ] Added a working directory argument to callCompiler.
773162c
nad added a commit that referenced this issue Oct 25, 2022
@nad
Fixed #6194.
2e8feb1
nad added a commit that referenced this issue Oct 25, 2022
@nad
[ #6194 ] Added a working directory argument to callCompiler.
71f99d4
@nad nad closed this as completed in 87e7bb2 Oct 25, 2022
@andreasabel andreasabel mentioned this issue Oct 25, 2022
Closed
@nad nad added the documented-in-changelog Issues already documented in the CHANGELOG label Oct 25, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@nad nad

Labels
backend: ghc Haskell code generation backend ("MAlonzo") documented-in-changelog Issues already documented in the CHANGELOG type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.6.3
Development

No branches or pull requests
1 participant
@nad