Commit 407e78e7 authored by Ike Mulder's avatar Ike Mulder
Browse files

Updated installfiles

parent cc95469a
Pipeline #65425 passed with stage
in 14 minutes and 21 seconds
......@@ -144,7 +144,7 @@ INSTALLFILES = \
$(INSTALLVFILES) \
$(INSTALLGLOBFILES)
real-install:
real-install: $(INSTALLVOFILES)
@echo "INSTALL"
$(HIDE)code=0; for f in $(INSTALLFILES); do\
if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
......
......@@ -4,11 +4,12 @@ theories/hint_search/lemmas_biabd.v
theories/hint_search/search_abd.v
theories/hint_search/search_biabd.v
theories/env_utils.v
theories/heap_lang/atomic_instances_heaplang.v
theories/heap_lang/biabd_instances_heaplang.v
theories/heap_lang/class_instances_heaplang.v
theories/heap_lang/stepping_tacs.v
theories/solve_defs.v
theories/steps/drop_modal.v
theories/steps/solve_instances.v
theories/steps/introduce_hyp.v
theories/steps/introduce_var.v
theories/steps/local_post.v
......@@ -19,8 +20,30 @@ theories/steps/small_steps.v
theories/steps/solve_one.v
theories/steps/solve_sep.v
theories/steps/tactics.v
theories/steps/verify_tac.v
theories/symb_exec/defs.v
theories/symb_exec/weakestpre.v
theories/symb_exec/weakestpre_logatom.v
theories/symb_exec/spec_notation.v
theories/symb_exec/atom_spec_notation.v
theories/tele_utils.v
theories/util_classes.v
theories/util_instances.v
theories/proofmode_base.v
theories/lib/atomic.v
theories/lib/int_as_nat_diff.v
theories/lib/loc_map.v
theories/lib/ticket_cmra.v
theories/lib/except_zero.v
theories/lib/intuitionistically.v
theories/lib/tokenizable.v
theories/lib/frac_token.v
theories/lib/iris_hints.v
theories/lib/own_hints.v
theories/lib/own/proofmode_classes.v
theories/lib/own/proofmode_instances.v
theories/lib/own/validity_tactics.v
theories/lib/Z_cmra.v
theories/lib/greatest_laterable_fixpoint.v
theories/lib/laterable.v
theories/lib/persistently.v
opam-version: "2.0"
name: "automation"
name: "diaframe"
version: "~dev"
synopsis: "Automation for iris"
synopsis: "Diaframe: Automation for Iris"
maintainer: "Ike Mulder <me@ikemulder.nl>"
authors: "Ike Mulder <me@ikemulder.nl>"
homepage: "https://gitlab.mpi-sws.org/iris/automation/"
bug-reports: "https://gitlab.mpi-sws.org/iris/automation/-/issues"
homepage: "https://gitlab.mpi-sws.org/iris/diaframe/"
bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
depends: [
"coq-iris-heap-lang" {= "dev.2022-02-11.0.1bff65be"}
"coq-autosubst" {= "dev"}
]
build: [make "-j%{jobs}%"]
install: [make "real-install"]
dev-repo: "git+https://gitlab.mpi-sws.org/iris/automation.git"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/diaframe.git"
Supports Markdown
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