[isabelle-dev] Confusion about ML_file and SML_file

[Makarius]

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