Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Dependency cycle in code generator

view this post on Zulip Email Gateway (Aug 19 2022 at 15:28):

From: Lars Hupel <hupel@in.tum.de>
Hi Florian et. al.,

I just noticed a dependency cycle in the standard code setup:

export_code
sorted_list_of_set insert
in SML file "tmp/code"

This prints:

Dependency "sorted_list_of_set" -> type "set" would result in module
dependency cycle

If I change "SML" to "Haskell", it will emit code just fine, however GHC
will complain about the dependency cycle. (scalac will eat it just fine,
though.)

What can be done about that? (As a workaround, I could redefine
"sorted_list_of_set" somewhere else.)

Cheers
Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 15:29):

From: Jose Divasón <jose.divasonm@unirioja.es>
Hi Lars,

if you add a module_name, then code can be exported:

export_code
sorted_list_of_set insert
in SML module_name Foo file "tmp/code"

Best,
Jose

Last updated: Apr 23 2024 at 12:29 UTC