[isabelle-dev] Code generation: privacy of exported types in signatures

2017-04-09 Thread Frederic Tuong (Dr)
Dear all, The SML generated code of the following snippet is not well typed anymore since Isabelle 2014: datatype 'a A = aaa datatype 'a B = bbb "'a C A" and 'a C = ccc "'a B" This is because when computing types to be marked as not private (during the generation of the signature of A, B

Re: [isabelle-dev] Code generation: privacy of exported types in signatures

2017-04-15 Thread Frederic Tuong (Dr)
statement exactly look like? > > Two points to note anyway: > > * This question would belong to the user (published release) rather than > the development (ongoing changes to a central code repository) mailing list. > > * The implementation of code exports is an over-a

Re: [isabelle-dev] Problem with ocaml nums.cma on Cygwin64

2017-10-06 Thread Frederic Tuong (Dr)
I am not using Cygwin, but would it be related with this: https://caml.inria.fr/mantis/view.php?id=7268 https://github.com/alainfrisch/flexdll (Alain Frisch seems to be one of the persons maintaining flexdll...) Frédéric Fri, 6 Oct 2017 16:38:54 +0200, Makarius : > We are moving towards