From 843053be92b6671c766c1d10b659d6d1b05e1630 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 1 Feb 2019 16:09:40 +0100 Subject: [PATCH] avoid mapping '.' path --- .gitignore | 1 + _CoqProject | 3 ++- exercises/ex_04_parallel_add.v | 2 +- exercises/ex_05_parallel_add_mul.v | 2 +- solutions/ex_04_parallel_add.v | 2 +- solutions/ex_05_parallel_add_mul.v | 2 +- 6 files changed, 7 insertions(+), 5 deletions(-) diff --git a/.gitignore b/.gitignore index c5b8b42..4b9dae5 100644 --- a/.gitignore +++ b/.gitignore @@ -30,3 +30,4 @@ Makefile.coq* *.crashcoqide .coqdeps.d build-dep +_opam diff --git a/_CoqProject b/_CoqProject index d91a04b..ce803ba 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,5 @@ --Q . tutorial +-Q exercises exercises +-Q solutions solutions -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files exercises/ex_01_swap.v exercises/ex_02_sumlist.v diff --git a/exercises/ex_04_parallel_add.v b/exercises/ex_04_parallel_add.v index ff350eb..11bb29a 100644 --- a/exercises/ex_04_parallel_add.v +++ b/exercises/ex_04_parallel_add.v @@ -6,7 +6,7 @@ threads increase a reference that's initially zero by two, the result is four. From iris.algebra Require Import auth frac_auth. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import lib.par proofmode notation. -From tutorial Require Import ex_03_spinlock. +From exercises Require Import ex_03_spinlock. (** The program as a heap-lang expression. We use the heap-lang [par] module for parallel composition. *) diff --git a/exercises/ex_05_parallel_add_mul.v b/exercises/ex_05_parallel_add_mul.v index 2ef3dba..2f46dee 100644 --- a/exercises/ex_05_parallel_add_mul.v +++ b/exercises/ex_05_parallel_add_mul.v @@ -11,7 +11,7 @@ Contrary to the earlier exercises, this exercise is nearly entirely open. From iris.algebra Require Import auth frac_auth. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import proofmode notation lib.par. -From tutorial Require Import ex_03_spinlock. +From exercises Require Import ex_03_spinlock. Definition parallel_add_mul : expr := let: "r" := ref #0 in diff --git a/solutions/ex_04_parallel_add.v b/solutions/ex_04_parallel_add.v index 7830ee2..80f3127 100644 --- a/solutions/ex_04_parallel_add.v +++ b/solutions/ex_04_parallel_add.v @@ -6,7 +6,7 @@ threads increase a reference that's initially zero by two, the result is four. From iris.algebra Require Import auth frac_auth. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import lib.par proofmode notation. -From tutorial Require Import ex_03_spinlock. +From solutions Require Import ex_03_spinlock. (** The program as a heap-lang expression. We use the heap-lang [par] module for parallel composition. *) diff --git a/solutions/ex_05_parallel_add_mul.v b/solutions/ex_05_parallel_add_mul.v index 77a6e20..f63786f 100644 --- a/solutions/ex_05_parallel_add_mul.v +++ b/solutions/ex_05_parallel_add_mul.v @@ -11,7 +11,7 @@ Contrary to the earlier exercises, this exercise is nearly entirely open. From iris.algebra Require Import auth frac_auth. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import proofmode notation lib.par. -From tutorial Require Import ex_03_spinlock. +From solutions Require Import ex_03_spinlock. Definition parallel_add_mul : expr := let: "r" := ref #0 in -- GitLab