[Caml-list] Preview: B-tree library

[Caml-list] Preview: B-tree library

[Tom Ridge]

[-- Attachment #1: Type: text/plain, Size: 316 bytes --]

Dear All,

This may be of interest for people thinking about on-disk storage etc.

https://github.com/tomjridge/tjr_btree/

It is not really in state to release, hence the "preview".

It is the core library in the upcoming "ImpFS" filesystem which (with
SibylFS) comes from the "Future filesystems" project.

Thanks

[-- Attachment #2: Type: text/html, Size: 546 bytes --]

Re: [Caml-list] Preview: B-tree library

[Hendrik Boom]

On Thu, Mar 16, 2017 at 01:35:26PM +0000, Tom Ridge wrote:
> Dear All,
> 
> This may be of interest for people thinking about on-disk storage etc.
> 
> https://github.com/tomjridge/tjr_btree/
> 
> It is not really in state to release, hence the "preview".
> 
> It is the core library in the upcoming "ImpFS" filesystem which (with
> SibylFS) comes from the "Future filesystems" project.

The intereseting point about this syste is in the README:

tjr_btree is a B-tree library. The core is written in Isabelle/HOL and exported to 
OCaml

Does this mean something like that the code has been generated from a ormal proof 
of its correctness?

-- hendrik

> 
> Thanks
> 
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] Preview: B-tree library

[Frédéric Bour]

[-- Attachment #1: Type: text/plain, Size: 784 bytes --]

Hi Tom,

Thanks for sharing this project, this looks promising. It seems this is 
a proven library?

Do you have links to this "Future filesystems" project? (and maybe the 
other names you mentioned).

Cheers,
Fred

On 16/03/2017 14:35, Tom Ridge wrote:
> Dear All,
>
> This may be of interest for people thinking about on-disk storage etc.
>
> https://github.com/tomjridge/tjr_btree/
>
> It is not really in state to release, hence the "preview".
>
> It is the core library in the upcoming "ImpFS" filesystem which (with 
> SibylFS) comes from the "Future filesystems" project.
>
> Thanks
>
>
> _______________________________________________
> MirageOS-devel mailing list
> MirageOS-devel@lists.xenproject.org
> https://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel


[-- Attachment #2: Type: text/html, Size: 1904 bytes --]

Re: [Caml-list] Preview: B-tree library

[Tom Ridge]

[-- Attachment #1: Type: text/plain, Size: 1200 bytes --]

At the moment, there is only the SibylFS website:

https://sibylfs.github.io/

And the EPSRC grant description:

http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K022741/1

But when things are further down the line, I will put together a website
for ImpFS.

Thanks



On 16 March 2017 at 13:55, Frédéric Bour <frederic.bour@lakaban.net> wrote:

> Hi Tom,
>
> Thanks for sharing this project, this looks promising. It seems this is a
> proven library?
>
> Do you have links to this "Future filesystems" project? (and maybe the
> other names you mentioned).
>
> Cheers,
> Fred
> On 16/03/2017 14:35, Tom Ridge wrote:
>
> Dear All,
>
> This may be of interest for people thinking about on-disk storage etc.
>
> https://github.com/tomjridge/tjr_btree/
>
> It is not really in state to release, hence the "preview".
>
> It is the core library in the upcoming "ImpFS" filesystem which (with
> SibylFS) comes from the "Future filesystems" project.
>
> Thanks
>
>
> _______________________________________________
> MirageOS-devel mailing listMirageOS-devel@lists.xenproject.orghttps://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel
>
>
>

[-- Attachment #2: Type: text/html, Size: 2926 bytes --]

Re: [Caml-list] Preview: B-tree library

[Tom Ridge]

[-- Attachment #1: Type: text/plain, Size: 1752 bytes --]

On 16 March 2017 at 14:05, Tom Ridge <tom.j.ridge@googlemail.com> wrote:

>
>
> On 16 March 2017 at 13:53, Hendrik Boom <hendrik@topoi.pooq.com> wrote:
>
>> On Thu, Mar 16, 2017 at 01:35:26PM +0000, Tom Ridge wrote:
>> > Dear All,
>> >
>> > This may be of interest for people thinking about on-disk storage etc.
>> >
>> > https://github.com/tomjridge/tjr_btree/
>> >
>> > It is not really in state to release, hence the "preview".
>> >
>> > It is the core library in the upcoming "ImpFS" filesystem which (with
>> > SibylFS) comes from the "Future filesystems" project.
>>
>> The intereseting point about this syste is in the README:
>>
>> tjr_btree is a B-tree library. The core is written in Isabelle/HOL and
>> exported to
>> OCaml
>>
>> Does this mean something like that the code has been generated from a
>> ormal proof
>> of its correctness?
>>
>
> Not at this point. But yes, previous versions have had (often partial)
> formal proofs developed. So I would say that the code is likely to be
> pretty good from a correctness point of view. Obviously the full formal
> proof for the core would be desirable. But other projects can probably
> start using the code now, hence why I released it relatively early.
>
>
>>
>> -- hendrik
>>
>> >
>> > Thanks
>> >
>> > --
>> > Caml-list mailing list.  Subscription management and archives:
>> > https://sympa.inria.fr/sympa/arc/caml-list
>> > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> > Bug reports: http://caml.inria.fr/bin/caml-bugs
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>>
>
>

[-- Attachment #2: Type: text/html, Size: 3439 bytes --]

Re: [Caml-list] Preview: B-tree library

[Julian Parsert]

Or does anyone know where the core in Isabelle/HOL can be found?


On 2017-03-16 14:53, Hendrik Boom wrote:
> On Thu, Mar 16, 2017 at 01:35:26PM +0000, Tom Ridge wrote:
>> Dear All,
>>
>> This may be of interest for people thinking about on-disk storage etc.
>>
>> https://github.com/tomjridge/tjr_btree/
>>
>> It is not really in state to release, hence the "preview".
>>
>> It is the core library in the upcoming "ImpFS" filesystem which (with
>> SibylFS) comes from the "Future filesystems" project.
> The intereseting point about this syste is in the README:
>
> tjr_btree is a B-tree library. The core is written in Isabelle/HOL and exported to
> OCaml
>
> Does this mean something like that the code has been generated from a ormal proof
> of its correctness?
>
> -- hendrik
>
>> Thanks
>>
>> -- 
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs