search

ejgallego / ssrbit

A small library for Bit Sequences
3 stars 5 forks source link

Port ssrbit to Mathcomp 1.9.0 #1

Open anton-trunov opened 5 years ago

anton-trunov commented 5 years ago

I'm opening this issue as we discussed on Mathcomp's gitter channel.

I basically need a library to implement “safe” arithmetics (with functions like add and so on signalling underflows/oferflows), reason about the correctness of implementation and extract the safe functions into OCaml.

ejgallego commented 5 years ago

@anton-trunov , I'm looking into this now, but first, should we setup CI?

I think you are way more up to date than me on current practices.

ejgallego commented 5 years ago

@anton-trunov the base code works fine in 1.9.0 however CoqEAL which is a dependency seems not availabe for math-comp 1.9.0, and indeed I can't compile their master branch; so I guess we must wait.

See: https://github.com/CoqEAL/CoqEAL/pull/19

anton-trunov commented 5 years ago

I'm looking into this now, but first, should we setup CI?

Sure, I guess we could reuse coq-community's setup. WDYT?

ejgallego commented 5 years ago

Sure, I guess we could reuse coq-community's setup. WDYT?

Sounds good!