Commit 538d0804 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename osiris → actris.

parent a169cf57
-Q theories osiris -Q theories actris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/utils/auth_excl.v theories/utils/auth_excl.v
theories/utils/list.v theories/utils/list.v
......
From stdpp Require Import sorting. From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel proofmode. From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert. From iris.heap_lang Require Import assert.
From osiris.utils Require Import list compare spin_lock. From actris.utils Require Import list compare spin_lock.
Definition qenqueue : val := λ: "q" "v", #(). Definition qenqueue : val := λ: "q" "v", #().
Definition qdequeue : val := λ: "q", #(). Definition qdequeue : val := λ: "q", #().
......
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import excl auth list. From iris.algebra Require Import excl auth list.
From osiris.utils Require Import auth_excl list. From actris.utils Require Import auth_excl list.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Inductive side := Left | Right. Inductive side := Left | Right.
......
From iris.heap_lang Require Export proofmode notation. From iris.heap_lang Require Export proofmode notation.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From osiris Require Export proto_channel. From actris Require Export proto_channel.
From iris.proofmode Require Import coq_tactics reduction spec_patterns. From iris.proofmode Require Import coq_tactics reduction spec_patterns.
(* TODO: strip laters *) (* TODO: strip laters *)
......
From osiris.channel Require Export channel. From actris.channel Require Export channel.
From osiris.channel Require Import proto_model. From actris.channel Require Import proto_model.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth excl. From iris.algebra Require Import auth excl.
From osiris.utils Require Import auth_excl. From actris.utils Require Import auth_excl.
Export action. Export action.
Definition start_chan : val := λ: "f", Definition start_chan : val := λ: "f",
......
From stdpp Require Import sorting. From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel. From actris.channel Require Import proto_channel.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From osiris.utils Require Import list. From actris.utils Require Import list.
From osiris.examples Require Import sort. From actris.examples Require Import sort.
Definition loop_sort_service : val := Definition loop_sort_service : val :=
rec: "go" "c" := rec: "go" "c" :=
......
From osiris.channel Require Import proto_channel proofmode. From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation lib.spin_lock. From iris.heap_lang Require Import proofmode notation lib.spin_lock.
From osiris.utils Require Import list contribution. From actris.utils Require Import list contribution.
From iris.algebra Require Import gmultiset. From iris.algebra Require Import gmultiset.
Definition map_worker : val := Definition map_worker : val :=
......
From stdpp Require Import sorting. From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel proofmode. From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From osiris.utils Require Import list compare contribution. From actris.utils Require Import list compare contribution.
From osiris.examples Require Import map sort_elem sort_elem_client. From actris.examples Require Import map sort_elem sort_elem_client.
From iris.algebra Require Import gmultiset. From iris.algebra Require Import gmultiset.
From Coq Require Import SetoidPermutation. From Coq Require Import SetoidPermutation.
......
From stdpp Require Import sorting. From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel proofmode. From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From osiris.utils Require Import list compare. From actris.utils Require Import list compare.
Definition lmerge : val := Definition lmerge : val :=
rec: "go" "cmp" "ys" "zs" := rec: "go" "cmp" "ys" "zs" :=
......
From stdpp Require Import sorting. From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel proofmode. From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From osiris.utils Require Import list compare. From actris.utils Require Import list compare.
From osiris.examples Require Import sort. From actris.examples Require Import sort.
Definition sort_client : val := λ: "cmp" "xs", Definition sort_client : val := λ: "cmp" "xs",
let: "c" := start_chan sort_service in let: "c" := start_chan sort_service in
......
From stdpp Require Import sorting. From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel proofmode. From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert. From iris.heap_lang Require Import assert.
From osiris.utils Require Import list compare. From actris.utils Require Import list compare.
Definition cont := true. Definition cont := true.
Definition stop := false. Definition stop := false.
......
From stdpp Require Import sorting. From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel proofmode. From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert. From iris.heap_lang Require Import assert.
From osiris.utils Require Import list compare. From actris.utils Require Import list compare.
From osiris.examples Require Import sort_elem. From actris.examples Require Import sort_elem.
Definition send_all : val := Definition send_all : val :=
rec: "go" "c" "xs" := rec: "go" "c" "xs" :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment