| # |
| # Copyright 2016, NICTA |
| # |
| # This software may be distributed and modified according to the terms of |
| # the GNU General Public License version 2. Note that NO WARRANTY is provided. |
| # See "LICENSE_GPLv2.txt" for details. |
| # |
| # @TAG(NICTA_GPL) |
| # |
| |
| include ../../../../build-env.mk |
| |
| COGENT_FLAGS ?= |
| |
| all: cogent |
| L4V_ARCH=ARM $(ISABELLE) build -v -d . -d $(BUILD_ENV_MK_DIR) -d $(BUILD_ENV_MK_DIR)/autocorres -b BilbyFs |
| |
| cogent: |
| cogent --shallow-consts-desugar-tuples --shallow-desugar-tuples --proof-name=BilbyFs \ |
| --dist-dir="impl" --root-dir="$(BUILD_ENV_MK_DIR)" $(COGENT_FLAGS) \ |
| ../cogent/src/fsop.cogent |
| sync: cogent |
| L4V_ARCH=$(L4V_ARCH) $(ISABELLE) build -v -d . -d $(AC_DIR) -b BilbyFsSync |
| |
| iget: cogent |
| L4V_ARCH=$(L4V_ARCH) $(ISABELLE) build -v -d . -d $(AC_DIR) -b BilbyFsIget |
