larsrh

use anyhow::{Error, Result};
use bitflags::bitflags;
use std::convert::TryFrom;
use std::fs::Permissions;
use std::os::unix::fs::PermissionsExt;

bitflags! {
    #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
    pub struct Perms: u16 {
        const UR = 0o400;

larsrh

:- discontiguous nat/2.
:- discontiguous typ/2.

natlit(0, _).
natlit(X, s(N)) :-
    natlit(Y, N),
    X is Y + 1.

nat(lit(nat, X), s(N)) :- natlit(X, N).

larsrh

import $ivy.`org.scalacheck::scalacheck:1.14.0`

import org.scalacheck._
import org.scalacheck.Arbitrary._
import scala.reflect._

trait TypeWitness1 {
  type F[_]
  val name: String
  def lift[A](implicit arb: Arbitrary[A]): Arbitrary[F[A]]

larsrh

val cities1 = Map("Portugal" -> List("Lisbon"), "Spain" -> List("Madrid"))
val cities2 = Map("Portugal" -> List("Coimbra"))

cities1 |+| cities2

larsrh

:- dynamic running/2.
:- dynamic jobid/1.

jobid(0).

resource(node1, 1, linux).
resource(node2, 2, linux).
resource(node3, 1, macos).

capacity(Node, Capacity) :- resource(Node, Capacity, _).

larsrh

/*
 * implicit conversion ("view"): implicit def f(x: A): B
 * non-view implicit:            implicit def f(implicit x: A): B
 *
 * we can summon implicit conversions with `implicitly[A => B]`
 * we can't do that with non-view implicits
 * this macro provides the trait `Conditional[A, B]` that provides precisely that
 */

package conditional

larsrh

module Proofs

%default total

data Natural : Type where
    Zero : Natural
    Succ : Natural -> Natural

add : Natural -> Natural -> Natural
add Zero y = y

larsrh

Aid the ecosystem in upgrading to sbt 1.0.x

Proposer

Proposed by Lars Hupel.

Abstract

Scala 2.10 used to (and still has, to some extent), huge gravitas in the Scala ecosystem. To large parts, this was due to Spark and sbt supporting only 2.10. Spark has migrated to 2.11, and sbt 1.0.x is already there (the RCs are binary compatible).

larsrh

module Lambda

open FStar.Mul

val factorial: n:nat -> Tot (y:nat{y >= 1 /\ y >= n})
let rec factorial n =
  if n = 0 then
    1
  else
    n * factorial (n - 1)

larsrh

// can be used like this:
// addCompilerPlugin("local.whatever" %% "whatever-plugin" % "0.1-SNAPSHOT" classifier "assembly" cross CrossVersion.patch)

name := "whatever-plugin"

organization := "local.whatever"

scalaVersion := "2.12.0"
crossScalaVersions := Seq("2.12.0", "2.12.1", "2.11.8", "2.11.7", "2.11.6")