On 27/06/17 22:21, Wenda Li wrote: > Dear Isabelle developers, > > When I am porting some of my old code from Isabelle-2016 to Isabelle2016-1, I > have encountered a problem that the command “SML_file" does not accept a SML > file that contains the function “PolyML.IntInf.gcd”. By going through NEWS, I > found the following entry: > > * Low-level ML system structures (like PolyML and RunCall) are no longer > exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY. > > I am a little confused as I thought SML_file should accept Standard ML files > (rather than Poly/ML ones). > > By the ways, both SML_file and ML_file in Isabelle2016 accept > “PolyML.IntInf.gcd", while ML_file in Isabelle2016-1(and the development > version) accept this command. This further confused me, as I thought ML_file > is the command that compiles Poly/ML files and should reject > “PolyML.IntInf.gcd” in Isabelle2016-1 as suggested by NEWS.
This looks like a normal isabelle-users question. Isabelle is a development environment for proofs and programs, and developing applications in Isabelle/ML, Isabelle/Scala, Isabelle/Isar, Isabelle/HOL are all user-space development activities. In contrast, the isabelle-dev mailing list is for the development process of Isabelle itself, including administrative issues. (See also the front web page.) Nonetheless here are some brief notes on these user commands: * ML_file etc. refer to Isabelle/ML (e.g. the embrace-and-extend version of Standard ML that is provided by Isabelle). * SML_file refers to quite strict Standard ML, and the PolyML structure is not part of that. Isabelle/ML includes PolyML.IntInf, and later exposes its operations as Integer.gcd and Integer.lcm. You can use SML_import to access these in strict SML, e.g. see src/Tools/SML/Examples.thy (which is also available in the Documentation panel). Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev