Would it be possible for Mockk to support "real partial mocks" (as well as "real partial relaxed mocks", via a feature equivalent to Mockito's thenCallRealMethod() feature.

Expected Behavior

You can create a mock that has all functions mocked except for a specified method, via a DSL "an

With some help from @nikswamy , I am trying to write mutually recursive functions with decreases clauses.

Consider the following example: variable-arity trees with a label on each edge.

module L = FStar.List.Tot
noeq type tree =
| Leaf
| Node:
  (labels: list nat) -> // I should probably add a `L.noRepeats` refinement here, but this is irrelevant here
  (children: ((x: nat {x 

How do I include the Hacl* library in the lib folder when extracting my code to OCaml?

Currently I am stuck with this, which can extract successfully for F* codes only using the F* libraries.

fstar.exe  --z3cliopt 'timeout=600000' --use_hints --use_hint_hashes  --odir out --codegen OCaml <modulename>.fst
OCAMLPATH="../../fstar/bin" ocamlfind opt -package fstarlib -linkpkg -g  out/<m

When a user repeatedly checks a model, the current model should indicate a trend for the state space statistics compared to the previous run (snapshot). I.e. has the number of distinct states gone up, down, or remained the same...

I'm not really sure it's by design or not, LH fails to parse bounds which include the unit literal ().

{-@
    testee :: forall <
                p :: Int -> () -> Int -> Bool
              , q :: Int -> () -> Int -> Bool
              >.
              { n :: Int |- Int<p n ()> <: Int<q n ()> }
              Int
@-}
testee :: Int
testee = 42

Literals of the types

The controls are worded in a few different ways right now.

Most of them are affirmative:

No sensitive data is written to application logs.

But some are conditional:

The app’s local storage should be wiped after an excessive number of failed authentication attempts.

I propose to rewrite the second type to the first type:

The app’s local storage is wiped after an excessive nu

Plan biweekly check of code quality with https://codeclimate.com/ and add outputs in the spreadsheet named "immudb codeclimate results" available in the shared drive "CodeNotary Product"

Our Makefile.ghdl doesn't have the usual | tee $(SIM_BUILD)/sim.log at the end of the simulation command line nor any other option to that effect, so it doesn't produce a sim.log file at all.

Counter examples today show information in tables to invalidate the equivalence, but does not show the result of the queries that makes evident that difference. It would be great if you could add that.

Pre issue-raising checklist

I have already (please mark the applicable with an x):

• Upgraded to the latest Pact Broker OR
• Checked the CHANGELOG to see if the issue I am about to raise has been fixed
• Created an executable example that demonstrates the issue using either a:
  • Dockerfile
  • Git repository with a Travis or Appveyor (or similar) build

Software ve

VUnit.add_source_files_from_csv() only passes vhdl_standard kwarg to Library.add_source_file(). However, my file gatherer uses .ahd file extensions to denote altera, .xhd to denote xilinx, and so on. I need the file_type available at least so I can tell VUnit that those file types are still vhdl, but all arguments should be available.

The Sphinx documentation flow was extended by several sphinx and third party extensions. These extensions should be documented along with their modifications. A comprehensive syntax guide should be assembled, to collect all syntax notations at one place instead of dozens of third party documentation websites with partially poor usage descriptions.

Extensions list:

• Standard Sphinx extensi

Our documentation lives at https://pysmt.readthedocs.io/ .

Possible ideas to improve it:

• Try to go through the "Getting Started" section. Are all steps clear? Do you manage to run the example on your computer?
• The Tutorials section needs formatting. The examples live in examples/ and are included using .. literalinclude:: ../examples/basic.py. It would be nice to find a better way to better

It looks like the docs just talk about the C and Python APIs, and don't talk about the command line tools.

I'm using ed25519-dalek for keygen, signing, and verification, and x25519 for ECDH. How do I convert secret public keys between them?

Take this naive attempt -- it seems like this works fine:

extern crate ed25519_dalek;
extern crate x25519_dalek;
extern crate rand;

use rand::prelude::*;

fn main() {
    let edkey1 = ed25519_dalek::Keypair::generate(&mut thread_rng()).public;

Travis now supports both OS X and Windows (in addition to Ubuntu). We should update our Travis script to at least run all the regressions on OS X in addition to Ubuntu. Windows would be good to add at some point too I guess.

I'm using Ubuntu linux with a recent FStar and kreMLin from master.
When attempting to run: krml -verbose Introduction.fst -no-prefix Introduction -o test.exe && ./test.exe
Where Introduction is the example from the kreMLin tutorial. I get this long error: