Previous week Up Next week

Hello

Here is the latest OCaml Weekly News, for the week of October 07 to 14, 2014.

  1. Self-containted OCaml distribution for Windows
  2. questions about merlin, vim and the Locate command
  3. OCaml projects for the FOSS Outreach Program
  4. Thoughts on targeting windows
  5. Macaque 0.7 and 0.7.1
  6. ppx_blob v0.1
  7. Core Suite 112.01.00 + rpc_parallel
  8. ppx_overload : ppx for user definable SML style overloading
  9. FoCaLiZe 0.9.0 released

Self-containted OCaml distribution for Windows

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-10/msg00034.html

Fabrice Le Fessant announced:
  We are pleased to announce the first beta release of our
self-contained OCaml distribution for Windows, "ocpwin-distrib". The
binary installer (71M) for ocpwin-distrib is available on:

https://github.com/OCamlPro/ocpwin-distrib

(read the README.md file).

"ocpwin-distrib" is an attempt at providing a self-contained
distribution of OCaml (currently, ocaml-4.01.0 + mingw + flexlink +
ocp-build) that does not need Cygwin to be used.

With this version (only 64-bit for now), you should be able to
install ocpwin-distrib in a directory you choose, and then start a
Windows command prompt (cmd) where all OCaml commands (except
ocamlbuild) should immediatly be available, both to compile in
bytecode and native code.

To provide a replacement for ocamlbuild, we provide both ocp-build and
a new '-make' option in ocamlc/ocamlopt that can be used to build
executable, libraries and pack files (see the documentation in the git
repo). omake should work as well, but is not yet provided.

You can use the Github issue tracker to fill a report on any bug you
find in this version.

Fabrice, for the OCamlPro team
      
Fabrice later added:
Just as a complement, we just pushed a new release fixing two issues:
- OCPWin now supports both 32 bits and 64 bits Windows platforms
- We clarified the license : you can freely redistribute significant
derivative works under your terms (commercial or non-commercial), as
long as you don't redistribute OCaml compiler parts (ocamlc/ocamlopt,
compiler-libs).
      

questions about merlin, vim and the Locate command

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-10/msg00036.html

Matej Kosik asked and ygrek replied:
> I have decided to check out Merlin
> and configure it with vim editor.
> There are two things I failed to figure out and I would be grateful for help.
> 
> (1)
> 
> When
> - I use the "Locate" command
> - and the corresponding definition is in the same ML-file
> then the cursors jumps to the definition.
> 
> Is backtracking supported?
> E.g., if you make 10 jumps forward, is it possible to gradually return where you started?
> (something similar to the "tag stack" maintained "ctags" / "otags")

The usual vim's Ctrl-O Ctrl-I works.

> (2)
> 
> When the corresponding definition is in a different ML-file
> then the current window is split into two windows
> (one for the original position
>  one with the requested definition)
> 
> Is there a way to prevent this window splitting?
> That is, an appropriate buffer at appropriate position would be displayed in the current window?

Put in ~/.vimrc

  let g:merlin_split_method = 'never'
      

OCaml projects for the FOSS Outreach Program

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-10/msg00044.html

Anil Madhavapeddy announced:
The Xen Project will be participating in Round 9 of the GNOME Outreach
Program, which aims to help groups that are underrepresented in free
and open source projects to get involved.  This was initially aimed at
female participants, but as a pilot is now being expanded to
participants in the Ascend Project.  It is a continuation of the very
successful GNOME Outreach Program for Women and we are running the
program in conjunction with GNOME and other prominent open source
projects.

There are further instructions here:
http://wiki.xenproject.org/wiki/OutreachProgram/Round9
https://wiki.gnome.org/OutreachProgramForWomen

You can find OCaml-related projects on the ideas list (primarily to do
with Mirage OS), but bear in mind that this list is not exhaustive.

http://wiki.xenproject.org/wiki/Outreach_Program_Projects

If there is an area that you would like to work on as an intern,
please get in touch with myself, Thomas Gazagnaire
<thomas.gazagnaire@cl.cam.ac.uk>, Dave Scott <dave.scott@citrix.com>
or Richard Mortier <richard.mortier@nottingham.ac.uk> directly to
discuss your ideas.

Two previous participants in the program last summer that worked on
OCaml and Mirage OS blogged about their experiences in depth:

 - Mindy Preston: http://www.somerandomidiot.com/blog/2014/08/22/opw-fin/
 - Jyotsna Prakash: http://1000hippos.wordpress.com/

Beginners are most welcome, but bear in mind that this round runs from
Dec 9th 2014 to March 9th 2014 and so will not work for full-time
students.  Full-time students should aim to apply for Round10 which
runs over the summer of 2015.
      

Thoughts on targeting windows

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-10/msg00045.html

Jeremy Yallop replied to Anil Madhavapeddy's message from last week:
> At a recent compiler hacking session in Cambridge, Don Syme pointed
> out a great Travis-like service for running regular Windows builds
> called Appveyor(.com).  In order to get more familiar with the Windows
> toolchain, I ported some of Thomas Braibant's instructions for
> compiling OPAM on Windows using it here:
>
> Cygwin scripts: https://github.com/ocaml/opam/blob/master/appveyor.yml
> Build output:   https://ci.appveyor.com/project/avsm/opam/build/1.0.38
>
> Appveyor can be used much like Travis and build every Git checkin on
> Windows, except that they unfortunately overwrite each other's
> status flags (the green tick or red cross against each commit), so
> they cannot be simultaneously used on one GitHub repository right
> now.  I contacted GitHub support and they indicated that they are
> adding support for multiple CI tools into the UI, but do not have
> a time estimate for when that would be ready.

I recently learnt of a solution to this issue: there's a third party
application which makes it possible to display both Travis and
AppVeyor build status flags on each commit:

   http://help.appveyor.com/discussions/kb/4-show-multiple-statuses-in-github-pull-requests

For example, on the following pull request

   https://github.com/yallop/ci-testing/pull/1

the status currently reads

   "Waiting to hear about 7e7a1ac — The Travis CI build passed /
Waiting for AppVeyor build to complete"

and links to a page with links to both the Travis and AppVeyor builds:

   http://github-multi-status.herokuapp.com/view?owner=yallop&repo=ci-testing&sha=7e7a1ac397a6eb3a5dc8937db4ea875617790280
      

Macaque 0.7 and 0.7.1

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-10/msg00051.html

Jacques-Pascal Deplaix announced:
We're happy to announce the double release of macaque 0.7 and 0.7.1.

Macaque is a type-safe and composable way to interact with SQL
databases from OCaml. We propose a form of "comprehension syntax" that
allow to modularly create queries in a strongly-typed and relatively
principled way.

Macaque is hosted on github at:

https://github.com/ocsigen/macaque

The packages are available on opam.

Those two new releases come with some features and tiny breaking changes.

The new main features are:
    - macaque now handles UNION, INTERSECT and EXCEPT:
       * Postgresql documentation:
http://www.postgresql.org/docs/9.3/static/queries-union.html
       * Macaque example: << union ({t.foo} | t in $table1$) ({t.foo}
| t in $table2$) ({t.foo} | t in $table3$) >>
    - new aggregate function: md5:
       * Postgresql documentation:
http://www.postgresql.org/docs/9.3/static/functions-string.html
       * Macaque example: << group {hash = md5[t.foo]} | t in $table$ >>
    - a new operator: IN:
       * Postgresql documentation:
http://www.postgresql.org/docs/9.3/static/functions-comparisons.html#AEN18448 

       * Macaque example: << {t.foo} | t in $table$; in' t.id $ids$ >>
(where ids being a list of postgresql integers)


Breaking changes:
    - We've fixed the type of current_timestamp so this should be
changed in your code (see the change bellow)
    - We've also changed the way of calling operators. So the
following code:
        <:table< table (
            date timestamp NOT NULL DEFAULT(current_timestamp)
         ) >>
      should have to change to something like:
        <:table< table (
            date timestamp NOT NULL DEFAULT(localtimestamp ())
         ) >>
      (The first change is about the name and the second about the
argument added)


Full details:

0.7.1:
    - Works with PGOCaml >= 2.0. int32_array is now mapped to int32
option array
    instead of int32 array

0.7:
    - Switch to OASIS
    - Add support for UNION, INTERSECT, EXCEPT and their UNION ALL variant
    - Add short types: nullable_data and non_nullable_data
    - Add support for SQL function/operators: md5, IN
    - Support unary operators (BREAKING CHANGE)
    - Current_timestamp now using timestamptz + adding localtimestamp
for timestamp
      

ppx_blob v0.1

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-10/msg00053.html

John Whitington announced:
Ppx_blob is an OCaml ppx to include a binary blob from a file as a
string. Writing [%blob "filename"] will replace the string with the
contents of the file at compile time. This allows the inclusion of
arbitary, possibly compressed, data, without the need to respect
OCaml's lexical conventions. This allows for smaller executables, and
a proper separation of data and code.

https://github.com/johnwhitington/ppx_blob

(Shortly with "opam install ppx_blob")

You will need OCaml version 4.02 or later.

For example, assuming the existence of "META" in the current directory:

        OCaml version 4.02.0

# #use "topfind";;
# #require "ppx_blob";;
# let meta = [%blob "META"];;
val meta : string =
  "name=\"ppx_blob\"\ndescription=\"Include a file as a string at
compile
time\"\nversion=\"0.1\"\nrequires=\"ppx_tools\"\nppx=\"./ppx_blob\"\n"

The example that comes with ppx_blob is the little quine:

print_string [%blob "quine.ml"]
      

Core Suite 112.01.00 + rpc_parallel

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-10/msg00056.html

Jeremie Dimino announced:
I am pleased to announce the 112.01.00 release of the Core suite.
Starting with this releases core packages require OCaml 4.02.

We are also releasing a new package: rpc_parallel. From the package
description:

Rpc_parallel offers an API to define various workers and protocols,
spawn workers as separate processes, and communicate with them using
Async Rpc.

The following packages were upgraded:

- async
- async_extended
- async_extra
- async_kernel
- async_unix
- bignum
- bin_prot
- core_bench
- core
- core_extended
- core_kernel
- custom_printf
- jenga
- ocaml_plugin
- rpc_parallel
- sexplib
- textutils
- type_conv

Files for this release are available on our website and all packages
are in opam:

https://ocaml.janestreet.com/ocaml-core/112.01.00/individual/

Unfortunately the documentation is not there yet due to opam-doc not
working with 4.02.

Here is list of changes for this version:

# 112.01.00

## async

- update tests

## async_extended

- Clarified an error in `Rpc_proxy`.

## async_extra

- Changed `Persistent_rpc_client.connected` to avoid returning a
connection that is closed at the time it was called.
- Optimized `Rpc.implement` so that if a server's implementation
returns a determined deferred, then the output is immediately
serialized and written out for the client.

This reduces memory consumption, improves throughput and latency.
Measurements with the `pipe_rpc_test program` showed that a server
went from processing 600\_000 msg/sec, to 2\_200\_000 msg/sec before
pegging the CPU.
- Changed `Log`'s output processor's batch size from `1_000` to `100`.
- Added `Persistent_rpc_client.close` and `close_finished`.
- In `Rpc.Connection.client` and `with_client`, used the
`handshake_timeout` as the `timeout` passed to `Tcp.connect`.

`handshake_timeout` was previously used only for the `Rpc` module's
handshake timeout.
- Changed `Rpc.create`'s `on_unknown_rpc` argument, renaming
`\`Ignore` as `\`Close_connection`, and requiring `\`Call` to return
`\`Close_connection` or `\`Continue`.

`\`Ignore` was renamed because it was a poor name, since in fact it
closed the connection.

Added a `\`Continue` option, whic allows one to keep the connection
open.

Changed `\`Call` to return `\`Continue` or `\`Close_connection`,
where the old `unit` return value meant `\`Close_connection`.
- In `Versioned_typed_tcp`, enabled the use of "credentials" in the
"Hello" message.

Propagate credentials to the user code when it arrives on the wire.

## async_kernel

- Optimized `Monitor.try_with ~run:\`Now f` to return a determined
deferred if `f ()` returns a determined deferred.

Previously, `Monitor.try_with ~run:\`Now f` always introduced a
`Deferred.map`, which made it impossible to do some optimizations
that bypass the scheduler overhead.
- Added an `ASYNC_CONFIG` field that causes the program to dump core
if Async jobs are delayed too much.

The new field is `dump_core_on_job_delay`.
- Switched `Async_kernel` from using `Core.Sys` to `Pervasives.Sys`
eliminating one of the dependencies on `Core`.

## async_unix

- Changed `Writer.transfer write pipe` to close `pipe` when the
`writer`, is closed.

Previously, `Writer.transfer` did not close the pipe when the
underlying writer is closed. This was strange because:

1. Callers would have to consistently check for the writer being
closed and close the `Pipe.Reader`t= themselves
2. The analogous function `Pipe.transfer` closes the reader on
similar circumstances.

The absence of the close was noticed as a bug in `Rpc`, which
assumed that `Writer.transfer` did the close.
- Fixed a bug in `Scheduler.yield` that caused it to pause for 50ms if
there is no other pending work and no I/O.
- Exposed type equivalence between `Unix.Passwd.t` and
`Core.Std.Unix.Passwd.t`.
- Changed `Writer.write_bin_prot` to use the new
`Bigstring.write_bin_prot`.

## bignum

- Added `Bignum.Bigint` module, with arbitrary-precision integers
based on `Zarith`, which is significantly faster than the
`Num.Big_int` library.

## bin_prot

- In `Write`, improved some OCaml macros to name values and avoid
calling C functions multiple times.

## core

- Removed vestigial code supporting OCaml 4.00.
- Added `Command` support for flags that are passed one or more times.

Added `Command.Spec.one_or_more` and
`Command.Spec.non_empty_sequence` to deal with the cases where you
expect a flag or anonymous argument (respectively) to be passed one
or (optionally) more times. This is common enough and distinct from
the case where you want the argument passed zero or more times that
it seems like we should canonize it in the library.
- In `Lock_file`, made stale lock detection more robust.

Made `Lock_file.create foo` succeed if `foo` is absent and
`foo.nfs_lock` file is present and stale. Previously, it would
fail.
- Removed `Syslog.syslog`'s `add_stderr` argument; use the `PERROR`
option instead.
- Fixed `unix_stubs.c` compilation on NetBSD

Closes #45
- Added `Filename` operators `/^` and `/@`, and `of_parts`, like the
same functions for Catalog paths.
- Changed `Iobuf` functions that advance the iobuf to not also return
a redundant number of bytes processed.

This avoids a small allocation (in the case of the `int option`
functions) and normalizes the result (so the same information isn't
returned two ways). Actually, it doesn't yet avoid the allocation in
the implementation, as the corresponding `Bigstring` functions must
still return the number of bytes processed, and currently do so as an
option. We hope to eventually change that.

In the future I expect we will change `unit` to some `error` variant
to also avoid the exception construction for `EWOULDBLOCK/EAGAIN`. We
can even make Unix syscalls `noalloc` if we're careful.
- In `Unix` module, added unit tests for `Cidr.does_match`.

## core_bench

- fixed legacy format string

## core_extended

- Added `Float_ref` module, which is like `float ref` but faster for
sets due to bypassing the write barrier.

Benchmark results on Sandy Bridge:

| [float\_ref.ml:] float ref set | 2\_886.94ns | 8.00w | |
| [float\_ref.ml:] Float\_ref.set | 355.76ns | 6.00w | |
| [float\_ref.ml:] float ref get | 415.52ns | 6.00w | |
| [float\_ref.ml:] Float_ref.get | 416.19ns | 6.00w | |
- Added `Bin_io_utils.Wrapped.t`, which defines an `'a t with bin_io`
that supports size-prefixed serialization and deserialization.

`Wrapped` has two useful submodules, `Opaque` and `Ignored`, for
efficient handling of size-prefixed bin-io values in cases where
serialization can be bypassed. See the comments in the module for
more details.

## core_kernel

- Removed vestigial code supporting OCaml 4.00.
- Used `{Hashable,Comparable}.S_binable` in `Day_of_week` and `Month`.
- Improved the performance of `Set_once.set`.
- Added `Type_equal.Lift3` functor.
- Replaced occurrences of `Obj.magic 0` with `Obj.magic None`.

With the former the compiler might think the destination type is
always an integer and instruct the GC to ignore references to such
values. The latter doesn't have this problem as options are not
always integers.
- Made `String_id.of_string` faster.
- Added `Bigstring` functions for reading and writing the
size-prefixed bin-io format.

- `bin_prot_size_header_length`
- `write_bin_prot`
- `read_bin_prot`
- `read_bin_prot_verbose_errors`
- Added `{Info,Error}.to_string_mach` which produces a single-line
sexp from an `Error.t`.
- Added `{Info,Error}.createf`, for creation from a format string.
- Added new `Perms` module with phantom types for managing access
control.

This module supersedes the `read_only`, `read_write`, and
`immutable` phantom types, which are now deprecated, and will be
removed in the future. This module uses a different approach using
sets of polymorphic variants as capabilities, and contravariant
subtyping to express dropping capabilities.

This approach fixes a bug with the current phantom types used for
`Ref.Permissioned` in which `immutable` types aren't guaranteed to
be immutable:

```ocaml
let r = Ref.Permissioned.create 0
let r_immutable = (r : (int, immutable) Ref.Permissioned.t)
let () = assert (Ref.Permissioned.get r_immutable = 0)
let () = Ref.Permissioned.set r 1
let () = assert (Ref.Permissioned.get r_immutable = 1)
```

The bug stems from the fact that the phantom-type parameter is
covariant, which allows OCaml's relaxed value restriction to kick
in, which allows one to create a polymorphic value, which can then
be viewed as both immutable and read write. Here's a small
standalone example to demonstrate:

```ocaml
module F (M : sig
type +'z t
val create : int -> _ t
val get : _ t -> int
val set : read_write t -> int -> unit
end) : sig
val t : _ M.t
end = struct
let t = M.create 0
let t_immutable = (t : immutable M.t)
let () =
assert (M.get t_immutable = 0);
M.set t 1;
assert (M.get t_immutable = 1);
;;
end
```

The new approach fixes the problem by making the phantom-type
parameter contravariant, and using polymorphic variants as
capabilities to represent what operations are allowed.
Contravariance allows one to drop capabilities, but not add them.
- Added `Int.Hex` module, which has hexadecimal sexp/string
conversions.
- Added `Gc.major_plus_minor_words`, for performance reasons.

## custom_printf

- Fixed uses of `printf=-style`format strings that have unspecified
behavior in OCaml 4.02 and will become errors.
- Support substitution in format string (lost with 4.02 compatibility)

## jenga

- Don't show noisy `glob..changed` messages except with
`-show-glob-changed` flag.
- Support shared build rules via `${jenga}/share`.
- Detect cycle in dep scheme instead of hanging.
- Made standalone actions atomic, just like actions associated with
target files.

Running actions and recording the result in the persistent
`.jenga.db` should be performed atomically for standalone actions,
as it is for actions which are associated with target files

## ocaml_plugin

- Changed to not use `rm -r` when it is expected to remove one file.

## rpc_parallel

Initial import.

## sexplib

- Replaced occurrences of `Obj.magic 0` with `Obj.magic None`.

With the former the compiler might think the destination type is
always an integer and instruct the GC to ignore references to such
values. The latter doesn't have this problem as options are not
always integers.

## textutils

- Added `Ascii_table.Table_char`, to expose the special table border
characters.

## type_conv

- Updated ast matching for 4.02
      

ppx_overload : ppx for user definable SML style overloading

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-10/msg00057.html

Jun Furuse announced:
I have OPAM-released ppx_overload, a ppx for user definable SML style
overloading.

For example you can overload (+) and (+.) to Plus.(+) as follows:

module Plus = struct
  external (+) : 'a -> 'a -> 'a = "%OVERLOADED"
  module Int = struct
    let (+) = Pervasives.(+)
  end
  module Float = struct
    let (+) = Pervasives.(+.)
  end
end

Then Plus.(+) works for int and float additions!

It works as follows:

* Declaration of overloaded values by external "%OVERLOADED"
* List the instances with the same name in its sub modules.
* The uses of overloaded values are resolved to one of their instances
at typing phase.

The overloading of ppx_overload is pretty limited: you cannot derive
overloading by using overloaded values polymorphicially. You cannot
define overloaded double with the overloaded Plus.(+). But still it is
a very interesting ppx example to combine with the OCaml typing.

ppx_overload is now available in OPAM. More detailed explanation how
it works is explained in the project page:
https://bitbucket.org/camlspotter/compiler-libs-hack . Enjoy!
      
Peter Zotov then said:
> Unfortunately this ppx trick does not work for the toplevel. It is
> since OCaml toplevel
> re-execute the ppx filter each time it gets a toplevel phrase. This
> makes the ppx filter
> hard to keep its state, in this case, the typing environment.

In 4.02.1 the toplevel allows the ppx rewriter to save some state.
See
http://caml.inria.fr/cgi-bin/viewvc.cgi/ocaml/trunk/parsing/ast_mapper.mli?view=markup#l192.
      
Alain Frisch added:
And sedlex ( https://github.com/alainfrisch/sedlex ) illustrates one
possible approach for storing the state.  Instead of marshaling in any
form some kind of internal state, it simply stores fragments of
parsetree (here, structure items) that impacted its internal state and
simply replay them on later phrases.  (This is not very efficient, but
for quick experiments in the toplevel, this is fine.)  I don't know if
this technique would apply to ppx_overload.
      
Jun Furuse then replied:
I do not think the ppx cookies can help ppx_overload in toplevel... It
requires typing environments which can be big. Maybe possible but
sounds odd.

In toplevel, it should be natural that ppx filters would keep living
along with the main toplevel process, rather than respawning it for
each toplevel phrase. But I understand the current design does not
permit such filter behavior.
      

FoCaLiZe 0.9.0 released

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-10/msg00066.html

François Pessaux announced:
It is my pleasure to announce the new release for FoCaLiZe (the
0.9.0 version).

A certain number of bugs found in the focalizec compiler have been fixed and
Zenon also had several issues fixed. Final let-definitions are now integrated.
The computation of dependencies has been deeply rewritten to compute them
*once* for all the possible backends (OCaml, Coq). Generated code is slightly
lighter and naming schemes and code generation schemes have been standardized
between OCaml and Coq.
A complete description of changes / new features can in found in the CHANGES
file of the distribution.

The 0.9.0 release is available from focalize.inria.fr at
http://focalize.inria.fr/download/focalize-0.9.0.tgz

Uncompress, extract, then read the INSTALL file in the newly created
directory focalize.0.9.0 and follow the simple instructions written there.


A public GIT repository is also available, allowing to fetch the latest
development state of FoCaLiZe. However, its content is not bullet-proof and
may be unstable at some times. It reflects the real-time state of FoCaLiZe
and may bring fixes and features not available in previous releases and that
will be part of the next release.
To clone the current FoCaLiZe GIT repository, invoke:
   git clone http://focalize.inria.fr/focalize.git
This will create a focalize repository in your current directory. Once cloned,
it is possible to fetch updates with the usual GIT commands (essentially git
pull origin master). Note that this access being public, it doesn't allow
pushing (i.e. submitting) modifications done in the sources tree.


To join people and discussions write to focalize-users@inria.fr.
Implementors also listen to suggestions (and compliments if some ^_^) at the
mail address: focalize-devel@inria.fr.

Enjoy.

For the entire FoCaLiZe implementation group,

François Pessaux.

October 2014

What is it FoCaLiZe ?
---------------------

FoCaLiZe is an integrated development environment to write high integrity
programs and systems. It provides a purely functional language to formally
express specifications, describe the design and code the algorithms.
Within the functional language, FoCaLiZe provides a logical framework to
express the properties of the code. A simple declarative language provides
the natural expression of proofs of properties them from within the program
source code.

The FoCaLiZe compiler extracts statements and proof scripts from the source
file, to pass them to the Zenon proof generator to produce Coq proof terms
that are then formally verified.

The FoCaLiZe compiler also generates the code corresponding to the
program as an Objective Caml source file. This way, programs developed in
FoCaLiZe can be efficiently compiled to native code on a large variety of
architectures.

Last but not least, FoCaLiZe automatically generates the documentation
corresponding to the development, a requirement for high evaluation
assurance.

The FoCaLiZe system provides means for the developers to formally express
their specifications and to go step by step (in an incremental approach) to
design and implementation, while proving that their implementation
meets its specification or design requirements. The FoCaLiZe language offers
high level mechanisms such as inheritance, late binding, redefinition,
parametrization, etc. Confidence in proofs submitted by developers or
automatically generated ultimately relies on Coq formal proof verification.

FoCaLiZe is a son of the previous Focal system. However, it is a completely
new implementation with vastly revised syntax and semantics, featuring a
rock-solid infrastructure and greatly improved capabilities.
      

Old cwn

If you happen to miss a CWN, you can send me a message and I'll mail it to you, or go take a look at the archive or the RSS feed of the archives.

If you also wish to receive it every week by mail, you may subscribe online.


Alan Schmitt