uwplse/verdi-raft issues and pull requests

#105 - update publication URLs

Pull Request - State: closed - Opened by palmskog 10 months ago

#104 - Dune-based extraction

Pull Request - State: open - Opened by palmskog 11 months ago

#103 - simplify proofs using conclude and conclude_using tactics

Pull Request - State: closed - Opened by palmskog 11 months ago

#102 - fix deprecations of intuition auto with star

Pull Request - State: closed - Opened by palmskog 11 months ago

#101 - reorganize files under standard theories directory

Pull Request - State: closed - Opened by palmskog 11 months ago

#100 - consistently use annotations

Pull Request - State: closed - Opened by palmskog 11 months ago

#99 - Consistently use From-Require to enable module relocation

Pull Request - State: closed - Opened by palmskog 11 months ago

#98 - consistently use bullets for goals in proofs

Pull Request - State: closed - Opened by palmskog 11 months ago

#97 - Fix deprecations

Pull Request - State: closed - Opened by palmskog 11 months ago

#96 - CI for 8.17 and later, drop configure script

Pull Request - State: closed - Opened by palmskog over 1 year ago

#95 - Adapt to Coq PR #17084: maximal implicit arguments now added by default to references in defined Ltac code.

Pull Request - State: closed - Opened by herbelin over 1 year ago

#94 - fix deprecations on 8.16 and later

Pull Request - State: closed - Opened by palmskog almost 2 years ago

#93 - Stop using ltac cast patterns

Pull Request - State: closed - Opened by SkySkimmer almost 2 years ago - 2 comments

#92 - add meta.yml, generate boilerplate

Pull Request - State: closed - Opened by palmskog almost 2 years ago

#91 - improved auto goal selection

Pull Request - State: closed - Opened by mrhaandi about 2 years ago

#90 - Adapt w.r.t. coq/coq#16004.

Pull Request - State: closed - Opened by ppedrot about 2 years ago

#89 - Trouble Building in Coq 8.10-8.12.2

Issue - State: closed - Opened by HazardousPeach over 2 years ago - 2 comments

#88 - Adapt to coq/coq#13837 ("apply with" does not rename arguments)

Pull Request - State: closed - Opened by SkySkimmer almost 3 years ago - 1 comment

#87 - Adapt to coq/coq#13837 ("apply with" does not rename arguments)

Pull Request - State: closed - Opened by SkySkimmer almost 3 years ago

#86 - Replace use of omega with lia for Coq 8.14 #13741

Pull Request - State: closed - Opened by jfehrle over 3 years ago - 1 comment

#85 - Fix w.r.t. coq/coq#12532.

Pull Request - State: closed - Opened by ppedrot over 4 years ago

#84 - Adapt w.r.t. coq/coq#12512.

Pull Request - State: closed - Opened by ppedrot over 4 years ago

#83 - compatibility with Coq PR 11906

Pull Request - State: closed - Opened by fajb over 4 years ago

#82 - Do not expect “firstorder” to solve arithmetic goals

Pull Request - State: closed - Opened by vbgl over 4 years ago

#81 - Minor cleaning

Pull Request - State: closed - Opened by vbgl almost 5 years ago - 2 comments

#80 - Proposal: verify Verdi Raft store interaction down to file system level

Issue - State: open - Opened by palmskog almost 5 years ago

#79 - Proposal: verify Raft handlers down to machine code level

Issue - State: open - Opened by palmskog almost 5 years ago

#78 - port to Coq master

Pull Request - State: closed - Opened by palmskog over 5 years ago

#77 - use Program Instance to avoid the soon-obsolete instance refinement mode

Pull Request - State: closed - Opened by palmskog over 5 years ago

#76 - Remove utility lemmas migrated elsewhere

Pull Request - State: closed - Opened by palmskog over 5 years ago

#75 - Add version of vard for use with the Oddity debugger

Pull Request - State: closed - Opened by dwoos about 6 years ago

#74 - attempt to fix issue where a Travis job uses the wrong commit

Pull Request - State: closed - Opened by palmskog over 6 years ago

#73 - Switch to using Docker images in Travis

Pull Request - State: closed - Opened by palmskog over 6 years ago

#72 - switch to strings for client ids and generate UUIDs in clients

Pull Request - State: closed - Opened by palmskog almost 7 years ago

#71 - client id type specified in Raft parameters

Pull Request - State: closed - Opened by palmskog almost 7 years ago

#70 - Allow any decidable type for request and client ids

Issue - State: closed - Opened by palmskog almost 7 years ago

#69 - Caching and 32-bit Coq in Travis

Pull Request - State: closed - Opened by palmskog almost 7 years ago

#68 - adapt to new approach where client sends id, introduce client reconnection

Pull Request - State: closed - Opened by palmskog almost 7 years ago

#67 - Correct handling of client ids

Pull Request - State: closed - Opened by dwoos almost 7 years ago - 1 comment

#66 - compatibility with both Coq 8.6.1 and 8.7.0

Pull Request - State: closed - Opened by palmskog almost 7 years ago

#65 - Proposal: store log count in log file

Issue - State: open - Opened by palmskog almost 7 years ago

#64 - Systems with log transformer

Pull Request - State: closed - Opened by palmskog almost 7 years ago

#63 - Extracted code uses Coq Ascii internals

Issue - State: closed - Opened by palmskog about 7 years ago

#62 - vard should signal when recovery from file fails

Issue - State: open - Opened by palmskog about 7 years ago

#61 - Adapt to Raft shim changes in client interface

Pull Request - State: closed - Opened by palmskog about 7 years ago

#60 - Verified serialization of network messages

Pull Request - State: closed - Opened by palmskog about 7 years ago

#59 - Capistrano-based deployment

Pull Request - State: closed - Opened by palmskog about 7 years ago - 1 comment

#58 - switch to safe_string for vard

Pull Request - State: closed - Opened by palmskog over 7 years ago

#57 - Simplify OPAM packages for Travis

Pull Request - State: closed - Opened by palmskog over 7 years ago

#56 - OPAM packages for Travis targets

Pull Request - State: closed - Opened by palmskog over 7 years ago

#55 - adapt to upstream changes to ghost simulation type classes

Pull Request - State: closed - Opened by palmskog over 7 years ago

#54 - Client-server marshaling allows users to inject commands and to crash the server

Issue - State: open - Opened by palmskog over 7 years ago

#53 - Server assumes that it can read the entire client request with a single recv call

Issue - State: open - Opened by palmskog over 7 years ago

#52 - Transient system call errors during recovery cause inconsistent re-initialization

Issue - State: open - Opened by palmskog over 7 years ago

#51 - Crash during update of snapshot causes loss of data

Issue - State: open - Opened by palmskog over 7 years ago

#50 - Server is unable to recover when disk log is incomplete due to a crash while writing an entry

Issue - State: open - Opened by palmskog over 7 years ago

#49 - Server crashes when trying to produce large packets because of buffer overflow

Issue - State: open - Opened by palmskog over 7 years ago

#48 - Transfer-based correctness theorem for Raft is missing

Issue - State: open - Opened by palmskog over 7 years ago

#47 - Fix some extraction warnings

Pull Request - State: closed - Opened by palmskog over 7 years ago

#46 - Set up OPAM package

Pull Request - State: closed - Opened by hackedy over 7 years ago

#45 - use consistent Verdi file layout

Pull Request - State: closed - Opened by palmskog over 7 years ago

#44 - VarDRaft.v belongs in systems directory

Issue - State: closed - Opened by palmskog over 7 years ago

#43 - port to Coq 8.6

Pull Request - State: closed - Opened by palmskog over 7 years ago - 4 comments

#42 - proof changes for failure semantics using update for reboot

Pull Request - State: closed - Opened by palmskog over 7 years ago - 1 comment

#41 - check that cluster size >= 2 in vard

Pull Request - State: closed - Opened by palmskog over 7 years ago - 1 comment

#40 - Node in singleton cluster never becomes leader

Issue - State: open - Opened by tbg over 7 years ago - 5 comments

#39 - use opam-dev repo in travis

Pull Request - State: closed - Opened by palmskog over 7 years ago

#38 - minor fixes in README.md, Makefile and Travis script

Pull Request - State: closed - Opened by palmskog over 7 years ago

#37 - Switch to verdi-runtime library and add OPAM compatibility

Pull Request - State: closed - Opened by palmskog over 7 years ago

#36 - Use Verdi namespace when importing Verdi files

Pull Request - State: closed - Opened by palmskog over 7 years ago

#35 - vard cluster members might not use the same cluster size

Issue - State: open - Opened by palmskog over 7 years ago

#34 - change vard to use cluster size based on command line parameters

Pull Request - State: closed - Opened by palmskog over 7 years ago

#33 - extracted files PHONY in main Makefile

Pull Request - State: closed - Opened by palmskog almost 8 years ago - 2 comments

#32 - Clients can livelock system

Issue - State: open - Opened by palmskog almost 8 years ago

#31 - Fix term handling in append entries reply

Pull Request - State: closed - Opened by dwoos almost 8 years ago - 1 comment

#30 - Fix inverted case handling in append entries reply on spec.

Pull Request - State: closed - Opened by spiliopoulos almost 8 years ago - 1 comment