lthms

#!/usr/bin/env stack
-- stack --resolver lts-10.4 script

import           Test.Hspec

sup :: Int -> Int
sup x
  | (x `mod` 10) /= 0 = x - (x `mod` 10) + 10
  | otherwise         = 10 * sup (x `div` 10)

lthms

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}

module Control.Monad.Chain.Fs
    ( -- * Functions
      openFile
    , closeFile
    , getLine
    , IO.IOMode(..)

lthms

Inductive sublist
          {A:  Type}
: list A -> list A -> Prop :=
| elem_hit (a:     A)
           (l l':  list A)
           (H:     sublist l l')
  : sublist (cons a l) (cons a l')
| elem_next (a:     A)
            (l l':  list A)
            (H:     sublist l l')

lthms

λ pijul pull lthms@nest.pijul.com:pointfree/pijul --from-branch refactorings                                                                                master pijul
Hash: AeHJpPsNz9ysK4b4otQVJfUMdBi0NeXSDndUwDNzDt3JSC8XjWTWxZbob1F-LWekLhszO10gt_8WwIB75NpMklY
Authors: ["pmeunier <pe@pijul.org>"]
Timestamp: 2017-09-01 07:01:18.120069075 UTC

    New Cargo.lock

Shall I pull this patch? [ynkad] n
Hash: AQwJmpxgfJ6yB9U3DL1Tui8WZfLBUbI_RK8zGyu5105CiUvvWnNvv9Kxw-GPEEA9pwFO3D8xM8J4hrEkXZRej1Q
Authors: ["pmeunier <pe@pijul.org>"]

lthms

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

module Vec where

data Nat = Z | S Nat

data Vector a n where
  VNil :: Vector a Z
  (:-) :: a -> Vector a n -> Vector a (S n)

lthms

* master
  * feat(nestling): get the list of branches of a given repository
    applied:
      * master
    deps:
  * feat(nestling): get the name of a branch
    applied:
      * master
    deps:
      * feat(nestling): get the list of branches of a given repository

lthms

DEBUG:pijul::commands: get_wd: None
DEBUG:pijul::commands: path: "/home/lethom/Repos/lkn"
DEBUG:libpijul::record: children of current_inode 0000000000000000
DEBUG:libpijul::record: iterating tree, starting from FileId { parent_inode: Inode(0000000000000000), basename: "" }
DEBUG:libpijul::record: calling record_all recursively, 397
DEBUG:libpijul::record: realpath: "/home/lethom/Repos/lkn/LICENSE"
DEBUG:libpijul::record: inode: Inode(141c73e142d55979)
DEBUG:libpijul::record: header: Some(FileHeader { metadata: FileMetadata(420), status: Ok, key: Key { patch: PatchId 0x85d31085e7e911f0, line: LineId(0x0200000000000000) } })
DEBUG:libpijul::record: current_node=FileHeader { metadata: FileMetadata(420), status: Ok, key: Key { patch: PatchId 0x85d31085e7e911f0, line: LineId(0x0200000000000000) } }
DEBUG:libpijul::record: old_attr=FileMetadata(420),int_attr=Some(FileMetadata(420))

lthms

DEBUG:pijul::commands: get_wd: None
DEBUG:libpijul::file_operations: collecting Inode(0000000000000000),""
DEBUG:libpijul::file_operations: basename = ""
DEBUG:libpijul::file_operations: starting iterator, key=Inode(0000000000000000)
DEBUG:libpijul::backend: iter_tree: Some((FileId { parent_inode: Inode(0000000000000000), basename: "" }, None))
DEBUG:libpijul::backend: tree iter
DEBUG:libpijul::backend: tree iter: UnsafeFileId { parent_inode: Inode(0000000000000000), basename: "LICENSE" } Inode(141c73e142d55979)
DEBUG:libpijul::file_operations: iter: FileId { parent_inode: Inode(0000000000000000), basename: "LICENSE" } Inode(141c73e142d55979)
DEBUG:libpijul::file_operations: collecting Inode(141c73e142d55979),"LICENSE"
DEBUG:libpijul::file_operations: node = FileHeader { metadata: FileMetadata(420), status: Ok, key: Key { patch: PatchId 0x85d31085e7e911f0, line: LineId(0x0200000000000000) } }

lthms

(* No more subgoal, yet one obligation remains *)

Program Definition software_only
        {H E: Type}
        (h: H)
        (e: E)
        {pEv: E -> Prop}
        (pEv_dec: forall (e: E), { pEv e } + { ~ pEv e })
        (pTs: H -> { e: E | pEv e } -> Prop)
  := if pEv_dec e

lthms

#define _GNU_SOURCE

#include <sched.h>
#include <unistd.h>
#include <stdio.h>
#include <stdlib.h>
#include <sys/wait.h>

#define STACK_SIZE 0x20000