Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question on Cycle dependency error when export...


view this post on Zulip Email Gateway (Oct 16 2025 at 10:36):

From: wangsl <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle community,

I'm using the verified ODE solver authored by Fabian Immler from the AFP
for code generation:

export_code one_step_until_time_impl_aform in SML

then it produces the following error information:

Dependency "real" :: "metric_space" -> "real" :: "t4_space" would
result in module dependency cycle

I also tried the following:

definition "fs = one_step_until_time_impl_aform optnS 2
(init_ode_ops False False (the_odo e1_fas true_form)) x0 False 1"

value fs

It seems value generates code successfully but encounters an error at
run time, part of the compile information is shown below:

Warning: Value identifier (x) has not been referenced.
At (line 10565 of "generated code")
Warning: Value identifier (dummy) has not been referenced.
At (line 10669 of "generated code")
Exception- Fail "division not by 2" raised

Has anyone encountered similar cycle dependency issues when exporting
code from the verified ODE solver or similar AFP entries? Are there
known workarounds for such export problems, particularly for numerical
ODE solvers? I've observed that in the Isabelle libraries that
metric_space is a subclass of t4_space, which aligns with our
mathematical understanding.

Also, does there exist pre-generated code implementations for this ODE
solver that we might have missed? We read Fabian Immler's work and
implementaton and only find tactics for proving bounds on exact
solutions of ODEs.

Thank you very much for your time and help.

Best regards,
Shuling Wang
Institute of Software, Chinese Academy of Sciences

view this post on Zulip Email Gateway (Oct 16 2025 at 11:19):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi,

I'm using the verified ODE solver authored by Fabian Immler from the AFP
for code generation:

export_code one_step_until_time_impl_aform in SML

then it produces the following error information:

Dependency "real" :: "metric_space" -> "real" :: "t4_space" would
result in module dependency cycle

Try

export_code one_step_until_time_impl_aform in SML module_name Example

instead

I also tried the following:

definition "fs = one_step_until_time_impl_aform optnS 2
(init_ode_ops False False (the_odo e1_fas true_form)) x0 False 1"

value fs

It seems value generates code successfully but encounters an error at
run time, part of the compile information is shown below:

Warning: Value identifier (x) has not been referenced.
    At (line 10565 of "generated code")
    Warning: Value identifier (dummy) has not been referenced.
    At (line 10669 of "generated code")
    Exception- Fail "division not by 2" raised

It seems this can only be answered by the author of the entry providing
that particular code setup
(https://www.isa-afp.org/entries/Affine_Arithmetic.html), which is also
Fabian Immler.

Cheers,
Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

view this post on Zulip Email Gateway (Oct 16 2025 at 11:19):

From: Manuel Eberl <manuel@pruvisto.org>
I don't know what this "division not by 2" error is about, but I can
tell you that the trick to solve the circular module dependency problem
is to do

export_code one_step_until_time_impl_aform in SML module_name Foo

where "Foo" is a name of your choice. That way, everything will be
exported into a single module and there will be no circular dependency
issues. If you export to a language like Haskell, this problem does not
arise at all since Haskell has no problem with circular dependencies.

Once you have successfully generated the code you can also search for
"division not by 2" in it and you might be able to figure out what the
issue is.

Manuel

On 16/10/2025 12:28, wangsl (via cl-isabelle-users Mailing List) wrote:

Dear Isabelle community,

I'm using the verified ODE solver authored by Fabian Immler from the
AFP for code generation:

export_code one_step_until_time_impl_aform in SML

then it produces the following error information:

Dependency "real" :: "metric_space" -> "real" :: "t4_space" would
result in module dependency cycle

I also tried the following:

definition "fs = one_step_until_time_impl_aform optnS 2
(init_ode_ops False False (the_odo e1_fas true_form)) x0 False 1"

value fs

It seems value generates code successfully but encounters an error at
run time, part of the compile information is shown below:

Warning: Value identifier (x) has not been referenced.
    At (line 10565 of "generated code")
    Warning: Value identifier (dummy) has not been referenced.
    At (line 10669 of "generated code")
    Exception- Fail "division not by 2" raised

Has anyone encountered similar cycle dependency issues when exporting
code from the verified ODE solver or similar AFP entries? Are there
known workarounds for such export problems, particularly for numerical
ODE solvers? I've observed that in the Isabelle libraries that
metric_space is a subclass of t4_space, which aligns with our
mathematical understanding.

Also, does there exist pre-generated code implementations for this ODE
solver that we might have missed? We read Fabian Immler's work and
implementaton and only find tactics for proving bounds on exact
solutions of ODEs.

Thank you very much for your time and help.

Best regards,
Shuling Wang
Institute of Software, Chinese Academy of Sciences

view this post on Zulip Email Gateway (Oct 18 2025 at 14:01):

From: Fabian Immler <fabian.immler@gmail.com>
Hi,

Glad to hear that you are trying to use my ODE solver :)

My AFP entries modify the code setup for type “real”: reals are represented
as float, and not rat (as in the Isabelle distribution).
In this code setup, division is only defined for powers of 2, and if your
code attempts to divide by something else, it raises this exception.

Did you perhaps specify some parameters in optnS (like stepsize or
tolerances) as a rational number (e.g. 0.1 or something like that)?

Code for the ODE solver is generated only internally for the
@{computation_check …} oracle in theory Example_Utilities. If you do an
export_code … in module …

for any of the constants involved in that oracle declaration, you should
get the “right” code generated (assuming you import Example_Utilities to
get the correct code setup).

Hope this helps, best wishes,

Fabian

On Thu, Oct 16, 2025 at 13:19 Florian Haftmann <florian.haftmann@cit.tum.de>
wrote:

Hi,

I'm using the verified ODE solver authored by Fabian Immler from the AFP
for code generation:

export_code one_step_until_time_impl_aform in SML

then it produces the following error information:

Dependency "real" :: "metric_space" -> "real" :: "t4_space" would
result in module dependency cycle

Try

export_code one_step_until_time_impl_aform in SML module_name Example

instead

I also tried the following:

definition "fs = one_step_until_time_impl_aform optnS 2
(init_ode_ops False False (the_odo e1_fas true_form)) x0 False 1"

value fs

It seems value generates code successfully but encounters an error at
run time, part of the compile information is shown below:

Warning: Value identifier (x) has not been referenced.
At (line 10565 of "generated code")
Warning: Value identifier (dummy) has not been referenced.
At (line 10669 of "generated code")
Exception- Fail "division not by 2" raised

It seems this can only be answered by the author of the entry providing
that particular code setup
(https://www.isa-afp.org/entries/Affine_Arithmetic.html), which is also
Fabian Immler.

Cheers,
Florian

view this post on Zulip Email Gateway (Oct 20 2025 at 01:23):

From: wangsl <cl-isabelle-users@lists.cam.ac.uk>
Thank you all for your assistance.

Following your suggestion, we have resolved the export_code question and
try to debug the resulting runtime error.
We are also checking if the error stems from the rational value setup in
optnS, as Fabian Immler (author of the ODE solver) mentioned in another
email.

Thanks,
Shuling

在 2025-10-16 19:19,Florian Haftmann 写道:

Hi,

I'm using the verified ODE solver authored by Fabian Immler from the
AFP for code generation:

export_code one_step_until_time_impl_aform in SML

then it produces the following error information:

Dependency "real" :: "metric_space" -> "real" :: "t4_space" would
result in module dependency cycle

Try

export_code one_step_until_time_impl_aform in SML module_name Example

instead

I also tried the following:

definition "fs = one_step_until_time_impl_aform optnS 2
(init_ode_ops False False (the_odo e1_fas true_form)) x0 False 1"

value fs

It seems value generates code successfully but encounters an error at
run time, part of the compile information is shown below:

Warning: Value identifier (x) has not been referenced.
    At (line 10565 of "generated code")
    Warning: Value identifier (dummy) has not been referenced.
    At (line 10669 of "generated code")
    Exception- Fail "division not by 2" raised

It seems this can only be answered by the author of the entry providing
that particular code setup
(https://www.isa-afp.org/entries/Affine_Arithmetic.html), which is also
Fabian Immler.

Cheers,
Florian


Last updated: Oct 20 2025 at 16:27 UTC