Skip to content
Snippets Groups Projects
Commit 7c06b30a authored by Simon Spies's avatar Simon Spies
Browse files

update coq project and opam

parent 0ad25f97
No related branches found
No related tags found
No related merge requests found
...@@ -11,39 +11,33 @@ ...@@ -11,39 +11,33 @@
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240). # We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths -arg -w -arg -ambiguous-paths
theories/algebra/ordinals/set_model.v theories/prelude/options.v
theories/algebra/ordinals/set_sets.v theories/prelude/prelude.v
theories/algebra/ordinals/set_functions.v theories/prelude/classical.v
theories/algebra/ordinals/set_ordinals.v
theories/algebra/ordinals/ord_stepindex.v
theories/algebra/ordinals/arithmetic.v theories/stepindex/stepindex.v
theories/stepindex/existential_properties.v
theories/stepindex/ordinals.v
theories/stepindex/ordinal_arith.v
theories/algebra/base.v
theories/algebra/stepindex.v
theories/algebra/monoid.v
theories/algebra/ofe.v theories/algebra/ofe.v
theories/algebra/monoid.v
theories/algebra/cmra.v theories/algebra/cmra.v
theories/algebra/updates.v theories/algebra/updates.v
theories/base_logic/base_logic.v
theories/program_logic/language.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
theories/bi/derived_laws_bi.v
theories/bi/derived_laws_sbi.v
theories/bi/satisfiable.v
theories/algebra/big_op.v theories/algebra/big_op.v
theories/algebra/auth.v theories/algebra/cmra_big_op.v
theories/algebra/frac_auth.v theories/algebra/numbers.v
theories/algebra/frac.v
theories/algebra/gmap.v theories/algebra/gmap.v
theories/algebra/truncation.v
theories/algebra/wf_IR.v theories/algebra/wf_IR.v
theories/algebra/cofe_solver.v theories/algebra/cofe_solver.v
theories/algebra/agree.v theories/algebra/agree.v
theories/algebra/excl.v theories/algebra/excl.v
theories/algebra/view.v
theories/algebra/auth.v
theories/algebra/functions.v theories/algebra/functions.v
theories/algebra/frac.v
theories/algebra/csum.v theories/algebra/csum.v
theories/algebra/list.v theories/algebra/list.v
theories/algebra/vector.v theories/algebra/vector.v
...@@ -54,62 +48,60 @@ theories/algebra/coPset.v ...@@ -54,62 +48,60 @@ theories/algebra/coPset.v
theories/algebra/proofmode_classes.v theories/algebra/proofmode_classes.v
theories/algebra/ufrac.v theories/algebra/ufrac.v
theories/algebra/namespace_map.v theories/algebra/namespace_map.v
theories/algebra/ufrac_auth.v
theories/algebra/dfrac.v theories/algebra/dfrac.v
theories/algebra/auth_map.v theories/algebra/lib/excl_auth.v
theories/algebra/auth_frac.v theories/algebra/lib/frac_agree.v
theories/algebra/mlist.v theories/algebra/lib/frac_auth.v
theories/bi/plainly.v theories/algebra/lib/gmap_view.v
theories/algebra/lib/mono_nat.v
theories/algebra/lib/ufrac_auth.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
theories/bi/derived_laws.v
theories/bi/derived_laws_later.v
theories/bi/big_op.v theories/bi/big_op.v
theories/bi/updates.v theories/bi/plainly.v
theories/bi/internal_eq.v
theories/bi/bi.v theories/bi/bi.v
theories/bi/tactics.v theories/bi/updates.v
theories/bi/embedding.v theories/bi/embedding.v
theories/bi/weakestpre.v theories/bi/ascii.v
theories/bi/satisfiable.v
theories/bi/telescopes.v theories/bi/telescopes.v
theories/bi/lib/fixpoint.v theories/bi/lib/fixpoint.v
theories/bi/lib/fractional.v theories/bi/lib/fractional.v
theories/base_logic/upred.v theories/base_logic/upred.v
theories/base_logic/bi.v theories/base_logic/bi.v
theories/base_logic/derived.v theories/base_logic/derived.v
theories/base_logic/algebra.v
theories/base_logic/proofmode.v theories/base_logic/proofmode.v
theories/base_logic/satisfiable.v theories/base_logic/base_logic.v
theories/base_logic/lib/iprop.v theories/base_logic/lib/iprop.v
theories/base_logic/lib/own.v theories/base_logic/lib/own.v
theories/base_logic/lib/saved_prop.v theories/base_logic/lib/saved_prop.v
theories/base_logic/lib/wsat.v theories/base_logic/lib/wsat.v
theories/base_logic/lib/invariants.v theories/base_logic/lib/invariants.v
theories/base_logic/lib/fancy_updates.v theories/base_logic/lib/fancy_updates.v
theories/base_logic/lib/logical_step.v theories/base_logic/lib/satisfiable.v
theories/base_logic/lib/viewshifts.v
theories/base_logic/lib/na_invariants.v theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/cancelable_invariants.v theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/gen_heap.v theories/base_logic/lib/gen_heap.v
theories/base_logic/lib/proph_map.v theories/base_logic/lib/proph_map.v
theories/program_logic/weakestpre.v
theories/program_logic/lifting.v
theories/program_logic/adequacy.v
theories/program_logic/hoare.v
theories/program_logic/ectx_language.v
theories/program_logic/ectxi_language.v
theories/program_logic/ectx_lifting.v
theories/program_logic/refinement/ref_source.v
theories/program_logic/refinement/ref_weakestpre.v
theories/program_logic/refinement/ref_adequacy.v
theories/program_logic/refinement/tc_weakestpre.v
theories/program_logic/refinement/seq_weakestpre.v
theories/program_logic/refinement/ref_lifting.v
theories/program_logic/refinement/ref_ectx_lifting.v
theories/heap_lang/locations.v
theories/heap_lang/lang.v
theories/heap_lang/metatheory.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/proofmode/base.v theories/proofmode/base.v
theories/proofmode/tokens.v theories/proofmode/tokens.v
theories/proofmode/modalities.v
theories/proofmode/ident_name.v
theories/proofmode/classes.v
theories/proofmode/class_instances.v
theories/proofmode/class_instances_later.v
theories/proofmode/class_instances_plainly.v
theories/proofmode/class_instances_updates.v
theories/proofmode/class_instances_internal_eq.v
theories/proofmode/class_instances_embedding.v
theories/proofmode/coq_tactics.v theories/proofmode/coq_tactics.v
theories/proofmode/ltac_tactics.v theories/proofmode/ltac_tactics.v
theories/proofmode/environments.v theories/proofmode/environments.v
...@@ -119,53 +111,5 @@ theories/proofmode/spec_patterns.v ...@@ -119,53 +111,5 @@ theories/proofmode/spec_patterns.v
theories/proofmode/sel_patterns.v theories/proofmode/sel_patterns.v
theories/proofmode/tactics.v theories/proofmode/tactics.v
theories/proofmode/notation.v theories/proofmode/notation.v
theories/proofmode/classes.v
theories/proofmode/class_instances_bi.v
theories/proofmode/class_instances_sbi.v
theories/proofmode/frame_instances.v theories/proofmode/frame_instances.v
theories/proofmode/modalities.v
theories/proofmode/modality_instances.v theories/proofmode/modality_instances.v
#################
### Examples
#################
# General Transfinite Iris
theories/examples/transfinite.v
# derived Hoare triples
theories/examples/refinements/derived.v
# key ideas
theories/examples/keyideas/simulations.v
theories/examples/keyideas/generalized_simulations.v
# Existing Safety Examples
theories/examples/safety/spawn.v
theories/examples/safety/par.v
theories/examples/safety/assert.v
theories/examples/safety/lock.v
theories/examples/safety/spin_lock.v
theories/examples/safety/ticket_lock.v
theories/examples/safety/nondet_bool.v
theories/examples/safety/counter.v
theories/examples/safety/lazy_coin.v
theories/examples/safety/clairvoyant_coin.v
theories/examples/safety/barrier/barrier.v
theories/examples/safety/barrier/proof.v
theories/examples/safety/barrier/specification.v
theories/examples/safety/barrier/example_client.v
# Termination Proofs
theories/examples/termination/adequacy.v
theories/examples/termination/thunk.v
theories/examples/termination/eventloop.v
theories/examples/termination/logrel.v
# Termination Preserving Refinement
theories/examples/refinements/refinement.v
theories/examples/refinements/memoization.v
# Some formalised counterexamples
theories/examples/counterexamples.v
...@@ -10,8 +10,8 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git" ...@@ -10,8 +10,8 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
synopsis: "This is the Coq development of the Iris Project" synopsis: "This is the Coq development of the Iris Project"
depends: [ depends: [
"coq" { (= "8.10.2") } "coq" { (= "8.15.1") }
"coq-stdpp" { (= "1.3.0") } "coq-stdpp" { (= "dev.2022-08-24.0.2c03acaf") | (= "dev") }
] ]
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment