We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
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
Compiler.Common.getCompileDataWith produces unused top-level definitions (at least for some primitive and prelude functions).
Compiler.Common.getCompileDataWith
Compile some program
module Main main : IO () main = do putStrLn "HelloWorld"
with dump compile data option
mkdir -p build/dump && \ time idris2 \ --source-dir src \ --dumpcases build/dump/def.named \ --dumplifted build/dump/def.lifted \ --dumpanf build/dump/def.anf \ --dumpvmcode build/dump/def.vmcode \ src/Main.idr && \
See some of dumps or result executable code cat build/dump/def.named
cat build/dump/def.named
No unused top-level definitions in dumped compile data and result executable:
Main.main = [{ext:0}]: (Prelude.IO.prim__putStr ["HelloWorld\n", !{ext:0}]) Prelude.IO.prim__putStr = Foreign call ["C:idris2_putStr, libidris2_support, idris_support.h", "node:lambda:x=>process.stdout.write(x)", "browser:lambda:x=>console.log(x)"] [String, %World] -> IORes Unit PrimIO.unsafePerformIO = [{arg:1}]: (PrimIO.unsafeCreateWorld [(%lam w (%let {eff:0} (!{arg:1} [!w]) !{eff:0}))]) PrimIO.unsafeCreateWorld = [{arg:1}]: (!{arg:1} [%MkWorld])
Unused top-level definitions:
prim__sub_Integer = [{arg:0}, {arg:1}]: (-Integer [!{arg:0}, !{arg:1}]) Main.main = [{ext:0}]: (Prelude.IO.prim__putStr ["HelloWorld\n", !{ext:0}]) Prelude.Types.prim__integerToNat = [{arg:0}]: (%case (<=Integer [0, !{arg:0}]) [(%constcase 0 0)] Just !{arg:0}) Prelude.EqOrd.compare = [{arg:0}, {arg:1}]: (%case (Prelude.EqOrd.< [!{arg:0}, !{arg:1}]) [(%constcase 1 0), (%constcase 0 (%case (Prelude.EqOrd.== [!{arg:0}, !{arg:1}]) [(%constcase 1 1), (%constcase 0 2)] Nothing))] Nothing) Prelude.EqOrd.== = [{arg:0}, {arg:1}]: (%case (==Integer [!{arg:0}, !{arg:1}]) [(%constcase 0 0)] Just 1) Prelude.EqOrd.< = [{arg:0}, {arg:1}]: (%case (<Integer [!{arg:0}, !{arg:1}]) [(%constcase 0 0)] Just 1) Prelude.EqOrd.compareInteger = [{ext:0}, {ext:1}]: (Prelude.EqOrd.compare [!{ext:0}, !{ext:1}]) Prelude.IO.prim__putStr = Foreign call ["C:idris2_putStr, libidris2_support, idris_support.h", "node:lambda:x=>process.stdout.write(x)", "browser:lambda:x=>console.log(x)"] [String, %World] -> IORes Unit PrimIO.unsafePerformIO = [{arg:1}]: (PrimIO.unsafeCreateWorld [(%lam w (%let {eff:0} (!{arg:1} [!w]) !{eff:0}))]) PrimIO.unsafeCreateWorld = [{arg:1}]: (!{arg:1} [%MkWorld])
The text was updated successfully, but these errors were encountered:
No branches or pull requests
Compiler.Common.getCompileDataWith
produces unused top-level definitions (at least for some primitive and prelude functions).Steps to Reproduce
Compile some program
with dump compile data option
See some of dumps or result executable code
cat build/dump/def.named
Expected Behavior
No unused top-level definitions in dumped compile data and result executable:
Observed Behavior
Unused top-level definitions:
The text was updated successfully, but these errors were encountered: