Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 25 Sep 1995 10:13:03 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA042117628;
          Mon, 25 Sep 1995 02:27:08 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from iraun1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA041977611;
          Mon, 25 Sep 1995 02:26:51 -0600
Received: from ira.uka.de (actually i80s16.ira.uka.de) by iraun1.ira.uka.de 
          with SMTP (PP); Mon, 25 Sep 1995 09:26:22 +0100
X-Mailer: exmh version 1.5.3 12/28/94
To: info-hol@leopard.cs.byu.edu
Cc: reetz@ira.uka.de
Subject: HOL90.7 does not build with SML/NJ 108
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Mon, 25 Sep 1995 09:26:08 +0100
From: reetz <reetz@ira.uka.de>
Message-Id: <"iraun1.ira.097:25.09.95.08.26.24"@ira.uka.de>

I fetched SML/NJ Version 108 basicly because it has a new garbage
collector [see FAQ of comp.lang.ml]. Unfortunately, HOL90.7 does not
build with SML/NJ 108 because of its dependency of the System module,
which has changed from 093 to 108 quite a bit.

Using grep, I found out that 74 (!) lines of the following 9 (!) modules
depend on the System module:

globals.sml
help.sml
lib.sml
parse_support.sml
pp.sml
save_hol.sml
sys_params.sml
gstack.sml
sys_lib.sml

I would like to propose to the HOL90 programmers that there should be
only ONE module containing all SML/NJ-specific functions. This would
make portability of HOL90 much easier and in general I think of not
only portability in respect of different SML/NJ-versions (imho that should
be the case, at least) but also to other sml-implementations like e.g.
moscow ml. During installation, the user may simply supply the name of
his/her sml and then the installation shell-script may choose the ONE fitting
module.

I furthermore would like to encourage the HOL90 programmers to drop the
depencendies of the sml/nj-specific System module as much as possible.
For example, imho it is not necessary to make save_hol.sml dependent on
function System.version:

save_hol.sml: * "Created on "^date^"using: " ^ System.version ^"\n\n\n"));
save_hol.sml:"Created on "^date^"using: " ^ System.version ^"\n\n\n"));

By the way, has anybody already adapted HOL90.7 to sml/nj 108?

Ralf.

(*******************************************************************)
(*                                                                 *)
(*  Ralf Reetz                                                     *)
(*                                                                 *)
(*  University of Karlsruhe                                        *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany              *)
(*                                                                 *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html       *)
(*  fax:    +49 721 370455                                         *)
(*  tel:    +49 721 6084220                                        *)
(*                                                                 *)
(*******************************************************************)