From: wangsl <cl-isabelle-users@lists.cam.ac.uk>
Hi Fabian,
Thank you for your response. Our work requires a rigorous numerical ODE
solver with adaptive step size control—precisely the ODE solver you have
implemented.
In our implementation, we import Example_Utilities and use the constant
function in oracle @{computation_check …} to generate code.
As you noted, we did specify some parameters in optnS as rational
numbers, and the error has just been resolved in the generated code
after we modified them to float.
Thanks again!
Best,
Shuling
在 2025-10-19 11:03,cl-isabelle-users-request@lists.cam.ac.uk 写道:
cl-isabelle-users digest Sun, 19 Oct 2025
Table of contents:
- 1 - Re: [isabelle] Question on Cycle dependency error when exporting
code
from verified ODE solver in AFP - Fabian Immler
<fabian.immler@gmail.com>
Message-ID:
<CAHBFu06z6RYGrw8m=puBeO_ZbY9itXzZUuG08770rVwD3NczKg@mail.gmail.com>
Date: Sat, 18 Oct 2025 16:00:46 +0200
From: Fabian Immler <fabian.immler@gmail.com>
Subject: Re: [isabelle] Question on Cycle dependency error when
exporting code
from verified ODE solver in AFPHi,
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 cycleTry
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" raisedIt 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
End of cl-isabelle-users Digest Sun, 19 Oct 2025
Last updated: Oct 20 2025 at 16:27 UTC