Stream: Miscellaneous

Topic: Standard ML vs (O)Caml


view this post on Zulip Karl Palmskog (Oct 06 2022 at 19:19):

Some interesting views here by Paulson on SML vs. (O)Caml, would be interesting to hear insiders comment...

for a functional language, let’s just say it’s odd that OCaml doesn’t have a streamlined syntax for (drum roll) declaring a function using pattern-matching

The main praise I remember of Caml in the 1990s was “it enjoys institutional support” (certainly true) and “it works with UNIX makefiles”

When I was porting HOL Light libraries, I occasionally had to replay a proof. I would have to launch OCaml, first thing in the morning. I could load the sources of HOL Light in under a minute. But the full analysis library would not finish loading until after lunch. This is a world-beating system?

they say that OCaml is finally catching up [to threads in Poly/ML], 15 years later, thanks to having 100 times as much funding.

view this post on Zulip Guillaume Melquiond (Oct 06 2022 at 19:57):

The first point is fair, though it is mostly a matter of taste; I for one do not care about such programming style. The second point is a bit distorted; the part about makefiles means that Caml code could be compiled to object files that could then be passed to the system linker; this was certainly seen as an improvement at the time. The third point conflates John's design decisions (e.g., using the bytecode repl) with the performance of OCaml; this is the most unfair of his points, in my opinion. The fourth point is the fairest one.

view this post on Zulip Enrico Tassi (Oct 06 2022 at 20:27):

Does OCaml have 100 times more users than polyml?

view this post on Zulip Enrico Tassi (Oct 06 2022 at 20:28):

(just one way to cut the crap)

view this post on Zulip Karl Palmskog (Oct 06 2022 at 20:30):

I guess we can use this to approximate relative users (Jan 2022): https://redmonk.com/sogrady/files/2022/03/lang-rank-0122-wm.png

SML is well behind Coq at this point on GitHub, OCaml is just trailing Haskell and Perl

view this post on Zulip Karl Palmskog (Oct 06 2022 at 20:34):

and it's a bit of a disappointment in the SML world that threads are not portable across compilers. But as an SML user, the lack of a widely used package manager is the worst pain point (this is the current best approximation)

view this post on Zulip Enrico Tassi (Oct 06 2022 at 20:36):

I don't think we should feed the troll

view this post on Zulip Karl Palmskog (Oct 06 2022 at 20:37):

fine by me, but I didn't even understand the point about Makefiles until Guillaume's comment.

view this post on Zulip Enrico Tassi (Oct 06 2022 at 20:39):

it's called separate compilation for the civilized ones

view this post on Zulip Enrico Tassi (Oct 06 2022 at 20:42):

(and I think some SML implementations do have it)

view this post on Zulip Enrico Tassi (Oct 06 2022 at 20:43):

it is really a trolling post

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 15:36):

Where is the trolling in the post? I can't pinpoint any specific part IMO that would count as a troll. There are some personal opinions, that's different.

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 17:50):

some writers like to separate opinions from facts more explicitly :-)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:01):

Paolo Giarrusso said:

some writers like to separate opinions from facts more explicitly :-)

what concrete phrase you have a problem with?

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 18:06):

I feel the tone is pretty biased beyond my literary criticism ability, but "This is a world-beating system?" is an example that I would object, say, in a paper peer review (just as a case where opinions _must_ be explicitly annotated)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:07):

Yup, Lawrence is quite biased that's obvious. But this is why I like to understand if he says something wrong or troll vs his own opinion.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:07):

The latter can't be addressed, the former yes

view this post on Zulip Théo Zimmermann (Oct 07 2022 at 18:07):

Does trolling implies saying something wrong?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):

In this case "this is a world beating system" I have to agree with him

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):

if that's the user experience for HOL , that's terrible

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):

tho it would be nice to ask for a clarification there

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):

to see he means HOL, not OCaml

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):

OCaml has its own problems

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:09):

when I migrated from Haskell I was far from impressed, and Haskell is not the 5th wonder of the world

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 18:09):

it also has very good things of course

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 18:12):

I can't define "troll" well enough to debate it, but he doesn't seem to believe in OCaml enough to be precise about what's going on. Of course, real problems exist :sweat_smile:

view this post on Zulip Théo Zimmermann (Oct 07 2022 at 18:16):

@Emilio Jesús Gallego Arias I think you are the only one who thinks he's talking about HOL here.

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 18:20):

here's why he blames OCaml for it:

With no way to save an image, you had to rebuild HOL Light from sources at every launch (even today). Even Edinburgh LCF was a stand-alone executable.

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 18:21):

somehow the option of doing <anything else than saving an image> isn't even worth mentioning — I mean, does Isabelle save images?

view this post on Zulip Karl Palmskog (Oct 07 2022 at 18:25):

SML can save a heap image for the state of any program, to my knowledge, so Isabelle uses them, see for example here: https://sketis.net/2017/isabelle-docker-image

view this post on Zulip Karl Palmskog (Oct 07 2022 at 18:27):

I don't know why HOL Light doesn't use native compilation in OCaml, I can't think of an obvious reason why one couldn't native-compile modules piecewise and then get a REPL on top that, but I've never seriously used HOL Light or the OCaml REPL

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 18:28):

I was mostly wondering why they can't compile sources to binaries and load the binaries, instead of reproving theorems

view this post on Zulip Théo Zimmermann (Oct 07 2022 at 18:28):

Maybe because of when HOL Light was created?

view this post on Zulip Karl Palmskog (Oct 07 2022 at 18:31):

from HOL Light README on GitHub:

There are now two alternatives: launch the OCaml toplevel and directly load the HOL Light source files into it, or create a standalone image with all the HOL Light sources pre-loaded. The latter is more convenient, but requires a separate checkpointing program, which may not be available for some platforms.

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 18:31):

yes, apparently, they're happy to link to _checkpointing tools_, which worries me a bit (maybe for no good reason)

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 18:32):

... I guess abstract types would force serialization into an LCF kernel, and somehow they're not willing to trust that, while trusting the checkpointing tool?

view this post on Zulip Karl Palmskog (Oct 07 2022 at 18:34):

this is apparently the checkpointing tool of preference these days: https://dmtcp.sourceforge.io/

view this post on Zulip Karl Palmskog (Oct 07 2022 at 18:39):

my understanding is that for most purposes, HOL Light could be called "John Harrison's HOL". If John doesn't need a feature (like convenient incremental compilation of theories) it doesn't get added

view this post on Zulip Enrico Tassi (Oct 07 2022 at 19:09):

http://www.catb.org/jargon/html/T/troll.html
1. v.,n. [From the Usenet group alt.folklore.urban] To utter a posting on Usenet designed to attract predictable responses or flames; or, the post itself.
... Some people claim that the troll (sense 1) is properly a narrower category than flame bait, that a troll is categorized by containing some assertion that is wrong but not overtly controversial. See also Troll-O-Meter.

Well, I stand by my analysis of the post.

view this post on Zulip Enrico Tassi (Oct 07 2022 at 19:11):

About separate compilation.

Take Coq: it has separate compilation. Loading two .vo is not super clear, e.g. their loading order is relevant (e.g. the last notation takes precedence). If you reason in term of heaps, then the order is fixed, either you user that heap or not. You can't merge heaps. That is much easier.

view this post on Zulip Enrico Tassi (Oct 07 2022 at 19:12):

I while ago I tried many snapshot systems, in the end I've used virtualbox. I let you imagine why.

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 19:17):

... because userspace checkpointing is fast, easy and correct? :smiling_devil:

view this post on Zulip Enrico Tassi (Oct 07 2022 at 19:17):

The last one, in particular ;-)

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 19:20):

in fairness, that's probably possible for a process doing just plain file I/O instead of opening sockets :sweat_smile:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:41):

Théo Zimmermann said:

Emilio Jesús Gallego Arias I think you are the only one who thinks he's talking about HOL here.

If not HOL what is he talking about? Clearly you can design a system in OCaml that doesn't require that time to load.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:43):

We recently invited Makarius to talk about the Isabelle build system and indeed heap images are pretty essential to what they do

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:45):

Anyways I don't see anything wrong or trollish in the post, other than indeed it addresses a very emotional and complex topic and of course he gives strong opinions but I wouldn't expect less of a professor of his level.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:49):

And for me, as part of this community, I'd rather avoid qualifying colleagues with adjectives such as "troll". As scientists we are free to disagree with other, but name-calling better not be based on vague interpretations that are far from consensual.

view this post on Zulip Paolo Giarrusso (Oct 08 2022 at 13:55):

Emilio Jesús Gallego Arias said:

If not HOL what is he talking about? Clearly you can design a system in OCaml that doesn't require that time to load.

he's blaming this HOL Light problem entirely on OCaml lacking images https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Standard.20ML.20vs.20.28O.29Caml/near/302910577.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:10):

In 1990 that was a very valid concern

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:11):

I don't see a problem with the phrasing "With no way to save an image, you had to rebuild HOL Light from sources at every launch (even today). Even Edinburgh LCF was a stand-alone executable." That was 100% accurate

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:11):

given the way these systems work

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:11):

it is a very valid concern, if you wanna do a HOL-style prover you better use PolyML these days

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:12):

Isabelle relies on this (and threading) extensively

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:12):

it is intrinsic to their design

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:13):

Indeed saving of state is a huge pain point in OCaml

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:13):

What we have in Coq with Marshall is just horrible and has many serious problems and limitations

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:14):

and prevents from doing very interesting stuff

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:14):

even in Coq today

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:14):

we don't support saving a proof session

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 14:14):

sorry that's horrible

view this post on Zulip Pierre Courtieu (Oct 08 2022 at 14:23):

Was there a ML dialect with images in 1990? If not then the point is moot.

view this post on Zulip Gaëtan Gilbert (Oct 08 2022 at 14:37):

Emilio Jesús Gallego Arias said:

we don't support saving a proof session

we had a Write State command, it got removed for some reason (cf 447965a9d4b409850e94a3289097ed28de8772fd)
since nobody complained it seems there were no users

view this post on Zulip Pierre Courtieu (Oct 08 2022 at 14:47):

Compiling files looked like a more principled way of speeding startup at that time I remember. It still looks like that to me today but I am not aware of how it works in other provers. Last time I discussed with Makarius he was happy with replaying the whole Isabelle standard lib with polyML in a few seconds (provided you had 3-4 cores/processors).

view this post on Zulip Karl Palmskog (Oct 08 2022 at 14:58):

Larry Paulson was using HOL Light just a few years ago to port things from the HOL Light stdlib to Isabelle. So he's not complaining about lack of heap images / checkpoint support in the 90s/2000s, he's complaining about it in modern OCaml.

view this post on Zulip Karl Palmskog (Oct 08 2022 at 15:04):

but my take would be that heap image support in Poly/ML has likely been maintained precisely because "big clients" (HOL4, Isabelle, ...) use it and require it. HOL Light could do without it, since it's even more niche than HOL4 and Isabelle, so therefore we get pointers in README to general Linux checkpointing tools.

view this post on Zulip Pierre Courtieu (Oct 08 2022 at 18:13):

@Emilio Jesús Gallego Arias what would be the benefits of such feature in ocaml? I am curious.

view this post on Zulip Pierre Courtieu (Oct 08 2022 at 18:13):

I mean for coq.

view this post on Zulip Karl Palmskog (Oct 08 2022 at 20:46):

one possibly-relevant data point: the colossus of the HOL4 world, CakeML, stopped using Poly/ML heap images as part of their regular builds a couple of years ago, and now uses an "incremental file-based build" similar to in Coq projects (Holmake in place of coq_makefile)


Last updated: Mar 28 2024 at 14:01 UTC