quinn-dougherty

Volsung tradition's curse flow

flowchart TD
    Andvari[Andvari]
    Hreidmar[Hreidmar]
    Regin[Regin]
    Fafnir[Fafnir]
    Otr[Otr]
    Dragon[Fafnir becomes dragon]

quinn-dougherty

#!/usr/bin/env python3
"""
Docker CVE Counter - Counts Docker-related CVEs by year

This script queries the National Vulnerability Database (NVD) API to find
Docker-related vulnerabilities and provides a yearly count breakdown.
"""

import requests
import json

quinn-dougherty

# install uv
curl -LsSf https://astral.sh/uv/install.sh | sh

# install nix
sh <(curl -L https://nixos.org/nix/install) --daemon

# enable flakes
mkdir -p /etc/nix
echo "experimental-features = nix-command flakes" >> /etc/nix/nix.conf

quinn-dougherty

import Lean.PrettyPrinter.Parenthesizer

/-
  live code in your own session
-/
#print Nat.rec

inductive tree (A : Type) : Type where
| leaf : A -> tree A
| node : tree A -> tree A -> tree A

quinn-dougherty

{
  description = "A PVS derivation in nix";
  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs";
    pvs = {
      url = "github:SRI-CSL/PVS";
      flake = false;
    };
  };
  outputs = { self, nixpkgs, pvs }: let

quinn-dougherty

generated  Oct 24, 2023 02:33:07
system     NixOS 23.11.20231011.5e4c2ad (Tapir) Linux 6.1.57
           x86_64
emacs      28.2
           /nix/store/v2cyn91ssjny8z9qwyq4zfjxbzx7xg9x-doom-emacs/      
           ->
           /nix/store/v2cyn91ssjny8z9qwyq4zfjxbzx7xg9x-doom-emacs/      
doom       3.0.0-dev fatal: not a git repository (or any of the
           parent directories): .git
           /nix/store/myh57gvlzi00v6sfk2fnyar98l30dbvs-doom-private/    

quinn-dougherty

From ExtLib Require Import Monad.

Section ArrowMonad.
  Context (A : Type).

  Instance CodArrowMonad : Monad (fun B => A -> B).
  Proof.
    constructor.
    - intros B y x.
      apply y.

quinn-dougherty

x = 1 to 2
y = {a: x, b: 1e1}
f(t) = normal(t, 1.1)
z = y.b * y.a

quinn-dougherty

// Needs to be able to import `PointSetTypes.pointSetDist` as `t` 
type scoreArgs = DistDist(t, t) | DistFloat(t, float), DistDistDist(t, t, t), DistFloatDist(t, float, t) 
// Can be expanded for the other 4 cases of the definition of scoring a scalar prediction against a dist answer.

module KlDivergence = {
  ...
} 

module LogScoreAgainstScalarAnswer = {
  let score = (prediction, answer) => ...

quinn-dougherty

let rec dispatchToGenericOutput = (
  call: ExpressionValue.functionCall,
  env: DistributionOperation.env,
): option<DistributionOperation.outputType> => {
  let (fnName, args) = call
  switch (fnName, args) {
 
... 
  | ("klDivergence", [EvDistribution(a), EvDistribution(b)]) =>
    Some(DistributionOperation.run(FromDist(ToScore(KLDivergence(b)), a), ~env))