From 19ece72598a5ff3f0547a32d1a507310e7ae72a2 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Fri, 16 Feb 2024 15:01:42 +0100 Subject: [PATCH] Automate initialization and installation of dependencies Ref. eng/recordflux/RecordFlux#1531 --- .gitignore | 1 + .gitlab-ci.yml | 10 +- Makefile | 433 ++++++++++++++++++++------------ Makefile.common | 21 +- doc/development_guide/index.rst | 50 ++-- rflx/ide/vscode/Makefile | 5 +- 6 files changed, 332 insertions(+), 188 deletions(-) diff --git a/.gitignore b/.gitignore index 2a8a9b0a5..bd795e559 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,7 @@ *.egg-info *.o *.pyc +.bin .coverage .coverage.* .env diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b92e05181..f8534b50f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -10,8 +10,6 @@ variables: SPARK_BUILD_DATE: "all" PYTHON_VERSION: "3.11" NODE_VERSION: "20.5.1" - POETRY_VERSION: "1.7.1" - POETRY_DYNAMIC_VERSIONING_VERSION: "1.2.0" # If set to 1, the packaging of RecordFlux including the compilation of the langkit-based parser will be tested. CLEAN_RECORDFLUX_SETUP: 0 @@ -59,8 +57,6 @@ workflow: .setup_python_venv: &setup_python_venv - export PATH=$HOME/.local/bin:$PATH - - pipx install poetry==$POETRY_VERSION - - pipx inject poetry poetry-dynamic-versioning==$POETRY_DYNAMIC_VERSIONING_VERSION - python$PYTHON_VERSION -m venv --clear .venv$PYTHON_VERSION - . .venv$PYTHON_VERSION/bin/activate - if [ "$SCHEDULE" = "nightly" ]; then @@ -77,6 +73,7 @@ setup: artifacts: paths: - .venv$PYTHON_VERSION + - .venv.poetry - alr - generated - rflx/lang @@ -99,8 +96,6 @@ setup: .setup_python: &setup_python - export PATH=/it/e3/bin:$PATH - export PATH=$HOME/.local/bin:$PATH - - pipx install poetry==$POETRY_VERSION - - pipx inject poetry poetry-dynamic-versioning==$POETRY_DYNAMIC_VERSIONING_VERSION - if [ $CLEAN_RECORDFLUX_SETUP -eq 1 ]; then python$PYTHON_VERSION -m venv --clear .venv; . .venv/bin/activate; @@ -110,9 +105,12 @@ setup: make init install_devel; fi else + ln -s .venv$PYTHON_VERSION .venv; . .venv$PYTHON_VERSION/bin/activate; make init; fi + # Prevent regeneration of Langkit-based parser + - touch generated/python/librflxlang generated/lib/relocatable/dev/librflxlang.so changelog: rules: diff --git a/Makefile b/Makefile index 0992078c5..4773a43da 100644 --- a/Makefile +++ b/Makefile @@ -2,46 +2,75 @@ include Makefile.common .DEFAULT_GOAL := all -VERBOSE ?= @ +# --- Parameters --- + TEST_PROCS ?= $(shell nproc) -RECORDFLUX_ORIGIN ?= https://github.com/AdaCore +DEVUTILS_ORIGIN ?= https://github.com/AdaCore GNATCOLL_ORIGIN ?= https://github.com/AdaCore LANGKIT_ORIGIN ?= https://github.com/AdaCore -ADASAT_ORIGIN?= https://github.com/AdaCore +ADASAT_ORIGIN ?= https://github.com/AdaCore VERSION ?= $(shell test -f pyproject.toml && test -f $(POETRY) && $(POETRY) version -s) -SDIST ?= dist/recordflux-$(VERSION).tar.gz -VSIX ?= rflx/ide/vscode/recordflux.vsix +NO_GIT_CHECKOUT ?= + +# --- Dependencies --- + +POETRY_VERSION = 1.7.1 +POETRY_DYNAMIC_VERSIONING_VERSION = 1.2.0 +POETRY_PLUGIN_EXPORT_VERSION = 1.6.0 -GENERATED_DIR = generated +# --- Repository structure --- + +PYTHON_PACKAGES := doc/language_reference/conf.py doc/user_guide/conf.py examples/apps language rflx tests tools stubs build.py +APPS := $(filter-out __init__.py,$(notdir $(wildcard examples/apps/*))) +SDIST = dist/recordflux-$(VERSION).tar.gz +VSIX = rflx/ide/vscode/recordflux.vsix +BIN_DIR := $(MAKEFILE_DIR)/.bin +GENERATED_DIR := generated BUILD_GENERATED_DIR := $(MAKEFILE_DIR)/$(BUILD_DIR)/$(GENERATED_DIR) -PYTHON_PACKAGES = doc/language_reference/conf.py doc/user_guide/conf.py examples/apps language rflx tests tools stubs build.py -DEVUTILS_HEAD = d36613dece1ec799fb550af1d0db5ea0d7aa94e1 + +# --- External repositories --- + +DEVUTILS_DIR = devutils +GNATCOLL_DIR = contrib/gnatcoll-bindings +LANGKIT_DIR = contrib/langkit +ADASAT_DIR = contrib/adasat + +DEVUTILS_HEAD = e7092e5a12ceb50af81fd7dec00f4d5353d1e6d2 GNATCOLL_HEAD = 25459f07a2e96eb0f28dcfd5b03febcb72930987 LANGKIT_HEAD = 65e2dab678b2606e3b0eada64b7ef4fd8cae91bb ADASAT_HEAD = f948e2271aec51f9313fa41ff3c00230a483f9e8 -SHELL = /bin/bash -POETRY_VENV = .venv.poetry -POETRY = $(POETRY_VENV)/bin/poetry +# --- Devutils --- + PYTEST = $(POETRY) run pytest -n$(TEST_PROCS) -vv --timeout=7200 RUFF = $(POETRY) run ruff BLACK = $(POETRY) run black MYPY = $(POETRY) run mypy --exclude rflx/lang KACL_CLI = $(POETRY) run kacl-cli -COMMON_DEPENDENCIES = $(POETRY) --include devutils/Makefile.common +DEVUTILS_DEPENDENCIES = $(RFLX) -APPS := $(filter-out __init__.py,$(notdir $(wildcard examples/apps/*))) +-include $(DEVUTILS_DIR)/Makefile.common + +# --- Environment variables --- export PYTHONPATH := $(MAKEFILE_DIR) +# --- Helper functions: Management of external repositories --- + # Switch to a specific revision of the git repository. # # @param $(1) directory of the git repository # @param $(2) commit id define checkout_repo -$(shell test -d $(1) && git -C $(1) fetch && git -C $(1) -c advice.detachedHead=false checkout $(2) > /dev/null) +$(if + $(wildcard $(1)), + $(if + $(shell git -C $(1) fetch && git -C $(1) -c advice.detachedHead=false checkout $(2) && echo 1), + , + $(error Checkout of "$(2)" in "$(1)" failed) + ) +) endef # Get the HEAD revision of the git repository. @@ -54,7 +83,7 @@ repo_head = $(shell test -d $(1) && git -C $(1) rev-parse HEAD || echo $(2)) # # @param $(1) directory of the git repository # @param $(2) expected revision -reinit_repo = $(if $(filter-out $(2),$(call repo_head,$(1),$(2))),$(call checkout_repo,$(1),$(2)),) +update_repo = $(if $(filter-out $(2),$(call repo_head,$(1),$(2))),$(call checkout_repo,$(1),$(2)),) # Remove the git repository, if no changes are present. # @@ -63,82 +92,203 @@ reinit_repo = $(if $(filter-out $(2),$(call repo_head,$(1),$(2))),$(call checkou # # @param $(1) directory of the git repository define remove_repo -$(if - $(or - $(shell test -d $(1) && git -C $(1) status --porcelain), - $(shell test -d $(1) && git -C $(1) log --branches --not --remotes --format=oneline) - ), - $(info Keeping $(1) due to local changes), - $(shell rm -rf $(1)) -) +((test -d $(1) && test -n "$$(git -C $(1) status --porcelain)") \ +|| (test -d $(1) && test -n "$$(git -C $(1) log --branches --not --remotes --format=oneline)")) \ +&& echo "Keeping $(1) due to local changes" \ +|| echo "Removing $(1)" && rm -rf $(1) endef -$(shell $(call reinit_repo,devutils,$(DEVUTILS_HEAD))) -$(shell $(call reinit_repo,contrib/gnatcoll-bindings,$(GNATCOLL_HEAD))) -$(shell $(call reinit_repo,contrib/langkit,$(LANGKIT_HEAD))) -$(shell $(call reinit_repo,contrib/adasat,$(ADASAT_HEAD))) +# --- Updating external repositories --- + +ifeq ($(NO_GIT_CHECKOUT), ) +$(shell $(call update_repo,$(DEVUTILS_DIR),$(DEVUTILS_HEAD))) +$(shell $(call update_repo,$(GNATCOLL_DIR),$(GNATCOLL_HEAD))) +$(shell $(call update_repo,$(LANGKIT_DIR),$(LANGKIT_HEAD))) +$(shell $(call update_repo,$(ADASAT_DIR),$(ADASAT_HEAD))) +endif + +# --- Default --- .PHONY: all all: check test prove -.PHONY: init deinit +# --- Setup --- -init: $(POETRY) devutils contrib/gnatcoll-bindings contrib/langkit contrib/adasat - $(VERBOSE)$(call checkout_repo,devutils,$(DEVUTILS_HEAD)) - $(VERBOSE)$(call checkout_repo,contrib/gnatcoll-bindings,$(GNATCOLL_HEAD)) - $(VERBOSE)$(call checkout_repo,contrib/langkit,$(LANGKIT_HEAD)) - $(VERBOSE)$(call checkout_repo,contrib/adasat,$(ADASAT_HEAD)) - $(VERBOSE)rm -f contrib/langkit/langkit/py.typed - $(MAKE) pyproject.toml +# `poetry install` always changes the modification time of `pyproject.toml`. To prevent a +# reinstallation on each invocation, `pyproject.toml` is added as an order-only dependency. +PROJECT_MANAGEMENT = $(POETRY) pyproject.toml.in $(DEVUTILS_DIR) | pyproject.toml +CONTRIB = $(GNATCOLL_DIR) $(LANGKIT_DIR) $(ADASAT_DIR) -deinit: - $(VERBOSE)$(call remove_repo,devutils) - $(VERBOSE)$(call remove_repo,contrib/gnatcoll-bindings) - $(VERBOSE)$(call remove_repo,contrib/langkit) - $(VERBOSE)$(call remove_repo,contrib/adasat) +.PHONY: init -$(POETRY): +init: $(CONTRIB) $(PROJECT_MANAGEMENT) + +# --- Setup: Poetry --- + +$(POETRY): $(POETRY_VENV) + $(POETRY_VENV)/bin/pip install poetry==$(POETRY_VERSION) poetry-dynamic-versioning==$(POETRY_DYNAMIC_VERSIONING_VERSION) poetry-plugin-export==$(POETRY_PLUGIN_EXPORT_VERSION) + +$(POETRY_VENV): python -m venv --clear $(POETRY_VENV) - $(POETRY_VENV)/bin/pip install poetry==1.7.1 poetry-dynamic-versioning==1.2.0 poetry-plugin-export==1.6.0 -devutils: - $(VERBOSE)git clone $(RECORDFLUX_ORIGIN)/RecordFlux-devutils.git devutils +pyproject.toml: pyproject.toml.in $(DEVUTILS_DIR) + cat pyproject.toml.in <(grep -v "^\[build-system\]\|^requires = \|^build-backend = \|^\[tool.setuptools_scm\]" $(DEVUTILS_DIR)/pyproject.toml) > pyproject.toml + +# --- Setup: External repositories --- + +$(DEVUTILS_DIR): +ifeq ($(NO_GIT_CHECKOUT), ) + git clone $(DEVUTILS_ORIGIN)/RecordFlux-devutils.git $(DEVUTILS_DIR) + git -C $(DEVUTILS_DIR) -c advice.detachedHead=false checkout $(DEVUTILS_HEAD) +endif + @test -d $(DEVUTILS_DIR) || (echo "$(DEVUTILS_DIR)" is missing; exit 1) + +contrib: + mkdir -p contrib + +$(GNATCOLL_DIR): | contrib +ifeq ($(NO_GIT_CHECKOUT), ) + git clone $(GNATCOLL_ORIGIN)/gnatcoll-bindings.git $(GNATCOLL_DIR) + git -C $(GNATCOLL_DIR) -c advice.detachedHead=false checkout $(GNATCOLL_HEAD) +endif + @test -d $(GNATCOLL_DIR) || (echo "$(GNATCOLL_DIR)" is missing; exit 1) + +$(LANGKIT_DIR): | contrib +ifeq ($(NO_GIT_CHECKOUT), ) + git clone $(LANGKIT_ORIGIN)/langkit.git $(LANGKIT_DIR) + git -C $(LANGKIT_DIR) -c advice.detachedHead=false checkout $(LANGKIT_HEAD) + rm -f $(LANGKIT_DIR)/langkit/py.typed +endif + @test -d $(LANGKIT_DIR) || (echo "$(LANGKIT_DIR)" is missing; exit 1) + +$(ADASAT_DIR): | contrib +ifeq ($(NO_GIT_CHECKOUT), ) + git clone $(ADASAT_ORIGIN)/adasat.git $(ADASAT_DIR) + git -C $(ADASAT_DIR) -c advice.detachedHead=false checkout $(ADASAT_HEAD) +endif + @test -d $(ADASAT_DIR) || (echo "$(ADASAT_DIR)" is missing; exit 1) + +# --- Setup: Build dependencies --- + +PYTHON_VERSION = $(shell test -f $(DEVEL_VENV)/bin/python && $(DEVEL_VENV)/bin/python --version | sed 's/Python \(3\.[0-9]*\)\.[0-9]*/\1/') +BUILD_DEPS = $(DEVEL_VENV)/lib/python$(PYTHON_VERSION)/site-packages/langkit + +$(BUILD_DEPS):: export PYTHONPATH= +$(BUILD_DEPS): $(CONTRIB) $(DEVEL_VENV) $(PROJECT_MANAGEMENT) + $(POETRY) install -v --no-root --only=build + +# --- Setup: Langkit-based parser --- + +PARSER = rflx/lang/librflxlang.so + +.PHONY: parser + +parser: $(PARSER) -contrib/gnatcoll-bindings: - $(VERBOSE)mkdir -p contrib - $(VERBOSE)git clone $(GNATCOLL_ORIGIN)/gnatcoll-bindings.git contrib/gnatcoll-bindings +$(PARSER): $(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so + mkdir -p rflx/lang + cp $(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so rflx/lang + cp $(GENERATED_DIR)/python/librflxlang/* rflx/lang + +$(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so: export GPR_PROJECT_PATH := \ + $(GPR_PROJECT_PATH):$(GENERATED_DIR)/langkit/langkit/support:$(GENERATED_DIR)/gnatcoll-bindings/gmp:$(GENERATED_DIR)/gnatcoll-bindings/iconv:$(GENERATED_DIR)/adasat +$(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so: export GNATCOLL_ICONV_OPT ?= -v +$(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so: $(wildcard language/*.py) $(GENERATED_DIR)/python/librflxlang + gprbuild -p -j0 -P$(GENERATED_DIR)/librflxlang.gpr \ + -XLIBRARY_TYPE=static-pic \ + -XLIBRFLXLANG_LIBRARY_TYPE=relocatable \ + -XLIBRFLXLANG_STANDALONE=encapsulated + +$(GENERATED_DIR)/python/librflxlang: export PYTHONPATH=$(MAKEFILE_DIR) +$(GENERATED_DIR)/python/librflxlang: $(BUILD_DEPS) $(wildcard language/*.py) | $(POETRY) + mkdir -p $(BUILD_GENERATED_DIR) + $(POETRY) run -- language/generate.py $(BUILD_GENERATED_DIR) $(VERSION) + cp -a $(MAKEFILE_DIR)/$(LANGKIT_DIR) $(BUILD_GENERATED_DIR)/ + cp -a $(MAKEFILE_DIR)/$(GNATCOLL_DIR) $(BUILD_GENERATED_DIR)/ + cp -a $(MAKEFILE_DIR)/$(ADASAT_DIR) $(BUILD_GENERATED_DIR)/ + rm -rf $(GENERATED_DIR) + mv $(BUILD_GENERATED_DIR) $(GENERATED_DIR) + +# --- Setup: Development dependencies --- + +.PHONY: install_devel + +install_devel: $(RFLX) + +$(RFLX):: export PYTHONPATH= +$(RFLX): $(DEVEL_VENV) $(CONTRIB) $(PARSER) $(PROJECT_MANAGEMENT) + $(POETRY) install -v --sync + +$(DEVEL_VENV): + python -m venv --clear $(DEVEL_VENV) + +# --- Optional setup: Installation from source distribution --- + +install:: export PYTHONPATH= +install: $(SDIST) $(PROJECT_MANAGEMENT) + $(POETRY) run pip install --force-reinstall $(SDIST) + +# --- Optional setup: Installation of FSF GNAT --- + +.PHONY: install_gnat printenv_gnat + +install_gnat: FSF_GNAT_VERSION ?= 11.2.4 +install_gnat: GPRBUILD_VERSION ?= 22.0.1 +install_gnat: + test -d build/alire || ( \ + mkdir -p build && \ + cd build && \ + alr -n init --lib alire && \ + cd alire && \ + alr toolchain --select --local gnat_native=$(FSF_GNAT_VERSION) gprbuild=$(GPRBUILD_VERSION) && \ + alr -n with aunit gnatcoll_iconv gnatcoll_gmp \ + ) + +printenv_gnat: + @test -d build/alire && (\ + cd build/alire && \ + alr printenv \ + ) || true -contrib/langkit: - $(VERBOSE)mkdir -p contrib - $(VERBOSE)git clone $(LANGKIT_ORIGIN)/langkit.git contrib/langkit +# --- Development environment --- -contrib/adasat: - $(VERBOSE)mkdir -p contrib - $(VERBOSE)git clone $(ADASAT_ORIGIN)/adasat.git contrib/adasat +.PHONY: activate deactivate -pyproject.toml: pyproject.toml.in devutils - cat pyproject.toml.in <(grep -v "^\[build-system\]\|^requires = \|^build-backend = \|^\[tool.setuptools_scm\]" devutils/pyproject.toml) > pyproject.toml +activate: $(BIN_DIR)/poetry + @echo . $(DEVEL_VENV)/bin/activate + @echo PATH=$$PWD/.bin:\$$PATH + +deactivate: + @echo deactivate + +$(BIN_DIR)/poetry: + @mkdir -p $(BIN_DIR) + @ln -sf $(POETRY) $(BIN_DIR) + +# --- Checks --- .PHONY: check check_poetry check_dependencies check_contracts check_doc -check: check_poetry check_dependencies common_check check_contracts check_doc +check: check_poetry check_dependencies check_contracts check_doc -check_poetry: $(POETRY) +check_poetry: $(RFLX) $(POETRY) check -check_dependencies: $(POETRY) +check_dependencies: $(RFLX) $(POETRY) run tools/check_dependencies.py -check_contracts: $(POETRY) +check_contracts: $(RFLX) $(POETRY) run pyicontract-lint $(PYTHON_PACKAGES) -check_doc: $(POETRY) +check_doc: $(RFLX) $(POETRY) run tools/check_doc.py -d doc -x doc/user_guide/gfdl.rst $(POETRY) run $(MAKE) -C doc/user_guide check_help $(POETRY) run tools/check_grammar.py --document doc/language_reference/language_reference.rst --verbal-map doc/language_reference/verbal_mapping.json examples/specs/*.rflx examples/apps/*/specs/*.rflx tests/data/specs/*.rflx tests/data/specs/parse_only/*.rflx $(POETRY) run tools/check_grammar.py --invalid --document doc/language_reference/language_reference.rst --verbal-map doc/language_reference/verbal_mapping.json tests/data/specs/invalid/{incorrect_comment_only,incorrect_empty_file,incorrect_specification}.rflx +# --- Tests --- + .PHONY: test test_rflx test_examples test_coverage test_unit_coverage test_language_coverage test_end_to_end test_property test_tools test_ide test_optimized test_compilation test_binary_size test_installation test_specs test_apps test: test_rflx test_examples @@ -151,38 +301,38 @@ test_examples: test_specs test_apps # Currently, pytest's CLI does not allow the specification of omitted directories # (cf. https://github.com/pytest-dev/pytest-cov/issues/373). -test_coverage: $(POETRY) +test_coverage: $(RFLX) timeout -k 60 7200 $(PYTEST) --cov=rflx --cov=tests/unit --cov=tests/integration --cov-branch --cov-fail-under=0 --cov-report= tests/unit tests/integration $(POETRY) run coverage report --fail-under=100 --show-missing --skip-covered --omit="rflx/lang/*" -test_unit_coverage: $(POETRY) +test_unit_coverage: $(RFLX) timeout -k 60 7200 $(PYTEST) --cov=rflx --cov=tests/unit --cov=tools --cov-branch --cov-fail-under=0 --cov-report= tests/unit tests/tools $(POETRY) run coverage report --fail-under=95.0 --show-missing --skip-covered --omit="rflx/lang/*" -test_language_coverage: $(POETRY) +test_language_coverage: $(RFLX) timeout -k 60 7200 $(PYTEST) --cov=rflx/lang --cov-branch --cov-fail-under=73.8 --cov-report=term-missing:skip-covered tests/language -test_end_to_end: $(POETRY) +test_end_to_end: $(RFLX) $(PYTEST) tests/end_to_end -test_property: $(POETRY) +test_property: $(RFLX) $(PYTEST) tests/property -test_tools: $(POETRY) +test_tools: $(RFLX) $(PYTEST) --cov=tools --cov-branch --cov-fail-under=43.6 --cov-report=term-missing:skip-covered tests/tools -test_ide: $(POETRY) +test_ide: $(RFLX) $(PYTEST) tests/ide # TODO(eng/recordflux/RecordFlux#1361): Execute `test` instead of `build` $(MAKE) -C rflx/ide/vscode check build -test_optimized: $(POETRY) +test_optimized: $(RFLX) PYTHONOPTIMIZE=1 $(PYTEST) tests/unit tests/integration tests/compilation -test_apps: +test_apps: $(RFLX) $(foreach app,$(APPS),$(MAKE) -C examples/apps/$(app) test || exit;) -test_compilation: $(POETRY) +test_compilation: $(RFLX) # Skip test for FSF GNAT to prevent violations of restriction "No_Secondary_Stack" in AUnit units [[ "${GNAT}" == fsf* ]] || $(MAKE) -C tests/spark build_strict $(MAKE) -C tests/spark clean @@ -197,12 +347,12 @@ test_compilation: $(POETRY) $(MAKE) -C tests/spark test_optimized $(MAKE) -C doc/examples build -test_binary_size: +test_binary_size: $(RFLX) $(MAKE) -C examples/apps/dhcp_client test_binary_size $(MAKE) -C examples/apps/spdm_responder test_binary_size test_specs: TEST_PROCS=1 -test_specs: $(POETRY) +test_specs: $(RFLX) $(PYTEST) tests/examples/specs_test.py test_installation: export PYTHONPATH= @@ -215,9 +365,7 @@ test_installation: $(SDIST) HOME=$(BUILD_DIR)/test_installation $(BUILD_DIR)/venv/bin/rflx install gnatstudio test -f $(BUILD_DIR)/test_installation/.gnatstudio/plug-ins/recordflux.py -fuzz_parser: FUZZER_RUNS=-1 -fuzz_parser: $(POETRY) - $(POETRY) run tools/fuzz_driver.py --state-dir $(BUILD_DIR)/fuzzer --corpus-dir $(MAKEFILE_DIR) --runs=$(FUZZER_RUNS) +# --- Tests: SPARK proofs --- .PHONY: prove prove_tests prove_python_tests prove_apps prove_property_tests @@ -227,61 +375,58 @@ prove_tests: $(GNATPROVE_CACHE_DIR) $(MAKE) -C tests/spark prove prove_python_tests: export GNATPROVE_PROCS=1 -prove_python_tests: $(GNATPROVE_CACHE_DIR) +prove_python_tests: $(RFLX) $(GNATPROVE_CACHE_DIR) $(PYTEST) tests/verification -prove_apps: $(GNATPROVE_CACHE_DIR) +prove_apps: $(RFLX) $(GNATPROVE_CACHE_DIR) $(foreach app,$(APPS),$(MAKE) -C examples/apps/$(app) prove || exit;) -prove_doc: +prove_doc: $(RFLX) $(MAKE) -C doc/examples prove -prove_property_tests: $(GNATPROVE_CACHE_DIR) +prove_property_tests: $(RFLX) $(GNATPROVE_CACHE_DIR) $(PYTEST) tests/property_verification -.PHONY: install install_devel install_build_deps install_git_hooks install_gnat printenv_gnat +# --- Fuzzing --- -install:: export PYTHONPATH= -install: $(POETRY) install_build_deps $(SDIST) - $(POETRY) run pip install --force-reinstall $(SDIST) +fuzz_parser: FUZZER_RUNS=-1 +fuzz_parser: $(RFLX) + $(POETRY) run tools/fuzz_driver.py --state-dir $(BUILD_DIR)/fuzzer --corpus-dir $(MAKEFILE_DIR) --runs=$(FUZZER_RUNS) -install_devel:: export PYTHONPATH= -install_devel: $(POETRY) install_build_deps parser - $(POETRY) install -v --sync +# --- Development tools --- -install_build_deps:: export PYTHONPATH= -install_build_deps: $(POETRY) pyproject.toml - $(POETRY) install -v --no-root --only=build +.PHONY: git_hooks -install_git_hooks: +git_hooks: install -m 755 tools/pre-{commit,push} .git/hooks/ -install_gnat: FSF_GNAT_VERSION ?= 11.2.4 -install_gnat: GPRBUILD_VERSION ?= 22.0.1 -install_gnat: - test -d build/alire || ( \ - mkdir -p build && \ - cd build && \ - alr -n init --lib alire && \ - cd alire && \ - alr toolchain --select --local gnat_native=$(FSF_GNAT_VERSION) gprbuild=$(GPRBUILD_VERSION) && \ - alr -n with aunit gnatcoll_iconv gnatcoll_gmp \ - ) - -printenv_gnat: - @test -d build/alire && (\ - cd build/alire && \ - alr printenv \ - ) || true - .PHONY: generate generate_apps -generate: +generate: $(RFLX) tools/generate_spark_test_code.py -generate_apps: +generate_apps: $(RFLX) $(foreach app,$(APPS),$(MAKE) -C examples/apps/$(app) generate || exit;) +.PHONY: anod_build_dependencies anod_poetry_dependencies + +anod_build_dependencies: $(POETRY) + @echo "requirements:" + @$(POETRY) export --with=build --without=dev --without-hashes | grep -v "@ file" | sed "s/\(.*\)/ - '\1'/" + @echo "platforms:" + @echo " - x86_64-linux" + +anod_poetry_dependencies: $(POETRY) + @echo "requirements:" + @echo " - 'poetry==$(POETRY_VERSION)'" + @echo " - 'poetry-dynamic-versioning==$(POETRY_DYNAMIC_VERSIONING_VERSION)'" + @echo " - 'poetry-plugin-export==$(POETRY_PLUGIN_EXPORT_VERSION)'" + @echo " - 'wheel'" + @echo "platforms:" + @echo " - x86_64-linux" + +# --- Documentation --- + .PHONY: doc html_doc pdf_doc doc: html_doc pdf_doc @@ -302,77 +447,41 @@ build_doc_language_reference: build_html_doc_language_reference build_pdf_doc_la build_html_doc: build_html_doc_language_reference build_html_doc_user_guide -build_html_doc_language_reference: +build_html_doc_language_reference: $(RFLX) $(MAKE) -C doc/language_reference html -build_html_doc_user_guide: +build_html_doc_user_guide: $(RFLX) $(MAKE) -C doc/user_guide html .PHONY: build_pdf_doc build_pdf_doc_language_reference build_pdf_doc_user_guide build_pdf_doc: build_pdf_doc_language_reference build_pdf_doc_user_guide -build_pdf_doc_language_reference: +build_pdf_doc_language_reference: $(RFLX) $(MAKE) -C doc/language_reference latexpdf -build_pdf_doc_user_guide: +build_pdf_doc_user_guide: $(RFLX) $(MAKE) -C doc/user_guide latexpdf +# --- Packaging --- + .PHONY: dist anod_dist dist: $(SDIST) -$(SDIST): $(POETRY) rflx/lang $(VSIX) pyproject.toml $(wildcard bin/*) $(wildcard rflx/*) +$(SDIST): $(BUILD_DEPS) $(PARSER) $(VSIX) pyproject.toml $(wildcard rflx/*) $(POETRY) build -vv --no-cache -f sdist -anod_dist: $(POETRY) rflx/lang pyproject.toml $(wildcard bin/*) $(wildcard rflx/*) +anod_dist: $(BUILD_DEPS) $(PARSER) pyproject.toml $(wildcard rflx/*) $(POETRY) build -vv --no-cache -anod_build_dependencies: $(POETRY) - @echo "requirements:" - @poetry export --with=build --without=dev --without-hashes | grep -v "@ file" | sed "s/\(.*\)/ - '\1'/" - @echo "platforms:" - @echo " - x86_64-linux" - -anod_poetry_dependencies: $(POETRY) - @echo "requirements:" - @echo " - 'poetry==1.7.1'" - @echo " - 'poetry-dynamic-versioning==1.2.0'" - @echo " - 'wheel'" - @echo "platforms:" - @echo " - x86_64-linux" +# --- Build: VS Code extension --- $(VSIX): @echo $(VSIX) $(MAKE) -C rflx/ide/vscode dist -.PHONY: parser - -parser: rflx/lang - -rflx/lang: $(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so - mkdir -p $@ - cp $(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so $@ - cp $(GENERATED_DIR)/python/librflxlang/* $@ - -$(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so: export GPR_PROJECT_PATH := \ - $(GPR_PROJECT_PATH):$(GENERATED_DIR)/langkit/langkit/support:$(GENERATED_DIR)/gnatcoll-bindings/gmp:$(GENERATED_DIR)/gnatcoll-bindings/iconv:$(GENERATED_DIR)/adasat -$(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so: export GNATCOLL_ICONV_OPT ?= -v -$(GENERATED_DIR)/lib/relocatable/dev/librflxlang.so: $(wildcard language/*.py) $(GENERATED_DIR)/python/librflxlang - gprbuild -p -j0 -P$(GENERATED_DIR)/librflxlang.gpr \ - -XLIBRARY_TYPE=static-pic \ - -XLIBRFLXLANG_LIBRARY_TYPE=relocatable \ - -XLIBRFLXLANG_STANDALONE=encapsulated - -$(GENERATED_DIR)/python/librflxlang: export PYTHONPATH=$(MAKEFILE_DIR) -$(GENERATED_DIR)/python/librflxlang: $(POETRY) $(wildcard language/*.py) pyproject.toml - mkdir -p $(BUILD_GENERATED_DIR) - $(POETRY) run -- language/generate.py $(BUILD_GENERATED_DIR) $(VERSION) - cp -a $(MAKEFILE_DIR)/contrib/langkit $(BUILD_GENERATED_DIR)/ - cp -a $(MAKEFILE_DIR)/contrib/gnatcoll-bindings $(BUILD_GENERATED_DIR)/ - cp -a $(MAKEFILE_DIR)/contrib/adasat $(BUILD_GENERATED_DIR)/ - rm -rf $(GENERATED_DIR) - mv $(BUILD_GENERATED_DIR) $(GENERATED_DIR) +# --- Clean --- .PHONY: clean clean_all @@ -385,6 +494,10 @@ clean: $(MAKE) -C rflx/ide/vscode clean $(MAKE) -C doc/examples clean -clean_all: - $(MAKE) clean - rm -rf $(GENERATED_DIR) rflx/lang pyproject.toml +clean_all: clean + rm -rf $(DEVEL_VENV) $(POETRY_VENV) $(BIN_DIR) $(GENERATED_DIR) rflx/lang pyproject.toml + test -d $(LANGKIT_DIR) && touch $(LANGKIT_DIR)/langkit/py.typed || true + @$(call remove_repo,$(DEVUTILS_DIR)) + @$(call remove_repo,$(GNATCOLL_DIR)) + @$(call remove_repo,$(LANGKIT_DIR)) + @$(call remove_repo,$(ADASAT_DIR)) diff --git a/Makefile.common b/Makefile.common index 177b04865..3a9cad64d 100644 --- a/Makefile.common +++ b/Makefile.common @@ -1,6 +1,23 @@ +# --- Repository structure --- + BUILD_DIR = build -MAKEFILE_DIR := $(dir $(abspath $(lastword $(MAKEFILE_LIST)))) -GNATPROVE = $(MAKEFILE_DIR)tools/gnatprove +MAKEFILE_DIR := $(abspath $(dir $(lastword $(MAKEFILE_LIST)))) + +# --- Virtual environments --- + +POETRY_VENV = $(MAKEFILE_DIR)/.venv.poetry +POETRY = $(POETRY_VENV)/bin/poetry + +DEVEL_VENV = $(shell test -n "$$VIRTUAL_ENV" && echo $$VIRTUAL_ENV || echo $(MAKEFILE_DIR)/.venv) +RFLX = $(DEVEL_VENV)/bin/rflx + +# --- Executables --- + +SHELL = /bin/bash + +# --- GNATprove --- + +GNATPROVE = $(MAKEFILE_DIR)/tools/gnatprove # Use GNATprove's file-based caching by default and ensure the directory exists. GNATPROVE_CACHE ?= file:$(MAKEFILE_DIR)$(BUILD_DIR)/gnatprove_cache diff --git a/doc/development_guide/index.rst b/doc/development_guide/index.rst index 11b4ac9b8..29f1c6e3d 100644 --- a/doc/development_guide/index.rst +++ b/doc/development_guide/index.rst @@ -19,23 +19,16 @@ The FSF GNAT and all Ada dependencies can be installed using Alire. $ make install_gnat $ eval `make printenv_gnat` -The configuration of the development tools is managed in a separate repository and must be downloaded and set up once. - -.. code:: console - - $ make init - -Poetry installs the Python project in a `virtual environment `_. +Set up the development environment. .. code:: console $ make install_devel -The virtual environment is activated by spawing a shell using Poetry. - -.. code:: console - - $ poetry shell +All other make targets that require an existing development environment (e.g. `make check`) will automatically download and install all required dependencies as well. +Some dependencies are managed in other git repositories and will be cloned during the initial setup. +The origin of these repositories can be changed by setting the respective variable (e.g., `DEVUTILS_ORIGIN`) appropriately either in the environment or directly in the initial call to `make`. +The initial setup can be repeated after resetting the repository with `make clean_all`. **Note:** An editable installation is used, so all changes to the Python source code take effect immediately and no reinstallation is required. @@ -56,11 +49,12 @@ Note, that this file has to be recreated whenever different tool versions are to Tools ===== +Make +---- + Make targets for common development tasks are: -- ``init`` Download and set up development configuration -- ``deinit`` Remove development configuration -- ``all`` Execute ``check``, ``test`` and ``prove`` +- ``all`` Execute ``check``, ``test`` and ``prove`` (default target) - ``check`` Run general checks and static code analysis tools for Python code - ``test`` Execute tests for Python code and SPARK code - ``prove`` Run GNATprove on SPARK tests and example apps @@ -68,13 +62,31 @@ Make targets for common development tasks are: - ``install_devel`` Install project in editable mode - ``doc`` Generate HTML documentation - ``dist`` Create Python package -- ``clean`` Remove all generated files -- ``clean_all`` Remove all generated files and editable installations +- ``clean`` Remove build directories and generated files +- ``clean_all`` Bring the repository to a completely clean state Additional tools can be found in ``tools/``. -Deterministic development and test environment -============================================== +Poetry +------ + +The Python project is managed by Poetry. +If there is no active virtual environment before executing the `make` commands, the Python project will be installed into a dedicated virtual environment named `.venv`. +If there is already an active virtual environment, RecordFlux will be installed into that virtual environment instead. +Poetry will always be installed into its own environment (`.venv.poetry`). + +It is not necessary to explicitly activate the virtual environments before executing any of the `make` targets. +They are used automatically during the execution of `make`. +However, in order to have the `rflx` command directly available in the shell, it is necessary to activate the project's virtual environment. +The following `make` targets can be used to respectively activate and deactivate it, as well as add or remove Poetry to/from the `PATH`. +Note the need to use `source <(...)` in the commands below. + +.. code:: console + + $ source <(make activate) + $ source <(make deactivate) + +Alternatively, RecordFlux can be executed also via Poetry by executing `.venv.poetry/bin/poetry run rflx`. Poetry locks the dependencies to ensure deterministic test results. `poetry lock` creates the lock file `poetry.lock` based on the dependencies listed in `pyproject.toml`. diff --git a/rflx/ide/vscode/Makefile b/rflx/ide/vscode/Makefile index c20b7d63b..ac9b3d645 100644 --- a/rflx/ide/vscode/Makefile +++ b/rflx/ide/vscode/Makefile @@ -1,4 +1,7 @@ +include ../../../Makefile.common + VSIX ?= recordflux.vsix +VERSION ?= $(shell $(POETRY) version -s | sed 's/\.dev/-dev/') .PHONY: all @@ -10,7 +13,7 @@ dist: $(VSIX) $(VSIX): export PATH := $(dir $(abspath Makefile))/node_modules/.bin:$(PATH) $(VSIX): node_modules out/extension.js - sed -i "s/\"version\": \".*\"/\"version\": \"$(shell poetry version -s | sed 's/\.dev/-dev/')\"/" package.json && vsce package -o recordflux.vsix && sed -i "s/\"version\": \".*\"/\"version\": \"0.0.0\"/" package.json + sed -i "s/\"version\": \".*\"/\"version\": \"$(VERSION)\"/" package.json && vsce package -o recordflux.vsix && sed -i "s/\"version\": \".*\"/\"version\": \"0.0.0\"/" package.json .PHONY: install