Skip to content
Snippets Groups Projects
Commit 6c83f2c8 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Forgot to add two files.

parent 2a0bc9c6
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
opam.pins
+ 1
− 1
View file @ 6c83f2c8
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0379384d795a443cb5ea31354644244f97a3299d coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b0418bd57b9341dbf5e58669c689201daa561bd7
theories/typing/unsafe/refcell/refcell.v
+ 1
− 1
View file @ 6c83f2c8
...@@ -6,7 +6,7 @@ From lrust.typing Require Import typing. ...@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Definition refcell_stR := Definition refcell_stR :=
optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) posR)). optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) positiveR)).
Class refcellG Σ := Class refcellG Σ :=
RefCellG :> inG Σ (authR refcell_stR). RefCellG :> inG Σ (authR refcell_stR).
......
  • Ralf Jung @jung ·
    Owner

    Could we please not have lambdaRust master depend on non-master Iris? This is the best way to get into a hell of a mess of various branches depending on each other in inscrutable ways. It also makes it hard e.g. to port lambdaRust to newer versions of Iris - which I am doing right now for the std++ port. CI fails, and there is little I can do because this depends on things that are not even in Iris master.

    If you want to use Iris features that are not yet merged, please do so in a feature branch of lambdaRust, and merge it into lambdaRust master only when the Iris things get merged.

  • Jacques-Henri Jourdan @jjourdan ·
    Maintainer

    Well, ok, if you prefer. But I am not sure have more branches will help simplifying the "mess of various branches depending on each other in inscrutable ways".

    Right now, for the std++ port, probably the best solution is to rebase the corresponding branch of Iris onto Iris master.

  • Ralf Jung @jung ·
    Owner

    But I am not sure have more branches will help simplifying the "mess of various branches depending on each other in inscrutable ways".

    Well, it will help for master -- "lambdaRust master always works with some commit from Iris master" is a very desirable invariant, IMHO. For example, it means that updating lambdaRust to use the latest Iris master commit is always "just" a matter of adapting to changes that have since happened in Iris. Considering that lambdaRust exercises many Iris features, that's a very useful thing to do when testing Iris changes. (This applies, e.g., to https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/39.)

    Edited by Ralf Jung
  • Ralf Jung @jung ·
    Owner

    All right, could you do the rebase please? I am having trouble here because I have a version of Iris with the prelude installed alongside stdpp, and somehow weird things are happening. Actually, I will have more fun later when I want to test the "options file" approach properly, i.e., loading the Iris options file from lambdaRust... I guess I'll just go back to an old lambdaRust locally and not pull until things have settled... so never mind the rebase.

    Edited by Ralf Jung
  • Jacques-Henri Jourdan @jjourdan ·
    Maintainer

    All right, could you do the rebase please?

    Done. Shall I merge your branch?

  • Ralf Jung @jung ·
    Owner

    You mean the stdpp branch? Sure, go ahead.

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