20 Commits

Author SHA1 Message Date
lhumphrey
fbc0e3eed9 Update proofs for Route Aggregator and Assignment Tree Branch and Bound (#41)
* Added missing test.out file for route_aggregator

* Updated proof session files for Route Aggregator and Assignment Tree Branch and Bound
2022-03-15 09:46:40 -04:00
M. Anthony Aiello
c087aac77b Merge pull request #37 from joffreyhuguet/silver_level_proof_algebra_tree
Silver level proof algebra tree
2021-10-28 15:14:41 -04:00
Joffrey Huguet
7bbdaa3c3e Update session files and proof testsuite 2021-10-25 17:40:25 +02:00
Joffrey Huguet
61b336ab7c Update session files and testsuite 2021-10-21 15:38:19 +02:00
Joffrey Huguet
99054911e4 Merge branch 'integration' into improve_proof_testsuite 2021-10-20 10:15:00 +02:00
Joffrey Huguet
ea0e4a2fd9 Improve run-proofs.py to allow to run on non-replay mode, to easily rewrite session files 2021-09-10 14:48:45 +02:00
Joffrey Huguet
57319a5a39 Update session files for CE2021 2021-07-26 17:47:38 +02:00
M. Anthony Aiello
5712513b30 Bootstrap Integration (#24)
* Integrate OpenUxAS-bootstrap into OpenUxAS

This commit represents a complete, working integration along with
several key enhancements. Note that the README is entirely unchanged and
not suitable.

***NOTE: the build will fail currently because of a problem with e3***
e3 provides no way to modify the list of excluded globs for sync_tree;
this will need to be fixed.

The bootstrap script works and will download and install needed support
for anod. The instructions printed at the end of the install are out of
date; the user doesn't need to do anything more than call anod with

    ./anod build uxas

The top-level anod script takes care of activating the python venv and
then calls the python anod script.

The user can also `source anod`, which will then register anod as a
shell function, allowing simpler invocation and a working setenv
command.

Anod's devel setup no longer supports uxas, since that's superfluous. It
does support lmcpgen and amase. They are placed in `develop` as before,
although finding a better name for the containing directory seems nice.

run-example works, as does resources/RunLmcpGen

make works

VS Code integration works

There is definite room for improvement. Specifically, factoring the
informtion about repository structure into some central set of
includable scripts seems like it should be really useful. Likewise,
anod's support should be a real python module so that it's easier to
use.

Finally, there's no reason not to automatically install the python venv
and all needed support the first time anod is invokved (including from
make). This would eliminate a needed step by the user. We could still
retain the bootstrap script if desired.

* Rename and create constants for repo structure

This commit reorganizes the directories a bit and introduces better
handling of pathnames through constants defined in paths.sh.
Unfortunately, because of the way python handles environment variables,
(and because we can't necessarily assume that python scripts are always
invoked through shell scripts that call paths.sh) we have to duplicate a
lot of the path information; this will hopefully be addressed in a
future commit.

* Refactor infrastructure and add github workflows.

OpenUxAS anod support is now a proper python module named `uxas`. Paths
within the uxas module are refactored. The module directory under
infrastructure/uxas has the expected layout for a python module project
and includes a tox.ini file so that tox can be used for development and
in CI.

infrastructure/install is now a script that calls into python scripts in
infrastructure/install-libexec; these are not a proper python module,
since that would create a chicken-and-egg problem. There is a tox.ini
file here, too, for development and CI.

infrastructure/bootstrap is the new bootstrap script, which is less
useful now but still usable.

Scripts have been updated as needed to take advantage of the uxas python
module. In particular, anod and run-example check for the python venv
and call into infrastructure/install if needed.

* Add Ada support and improve scripts

Added support for Ada back in by reactivating and updating
install-gnat.py Added Ada build-prove workflow

Refactored venv activation to paths.sh

Added ensure_gnat, which will check for gnat on the path (via which) or
will add a local install of GNAT CE to the path (if it's there) or will
offer to install GNAT CE via install-gnat.py This means the user can
always choose a different GNAT and it will be used; otherwise, the local
install of GNAT CE will be used.

Added wrapper shell scripts for the python testing and proof scripts so
that the environment can be automatically configured.

Updated the C++ workflow

Note: sourcing anod and then running anod as a shell function isn't
behaving quite right in either bash or zsh (and for different reasons).
Needs further investigation.

* Add debug output to print commands executed.

This should address concern that users won't be able to figure out what
the scripts are doing if things break and require manual intervention.

Also modify the workflows so that they will run if critical scripts are
updated.

* Enhance run-example to better search for binaries.

run-example now follows similar logic to run-tests in searching for
binaries. uxas and uxas-ada are also special-cased so that searching
locally and in anod should succeed as expected. The search order is:

1. path (using `which`)
2. local (obj/cpp/uxas or src/ada/uxas-ada)
3. anod (inside uxas-release or uxas-ada-release)

run-example also follows similar logic in search for OpenAMASE:

1. specified via argument
2. local (develop/OpenAMASE)
3. anod (inside amse)

I believe these have all been tested.

Help / error strings have been updated so that they are consistent with
the new infrastructure.

Debug output has been improved to be more consistent with that provided
by e3 (but doesn't actually directly use e3, still).

This commit also improves the .gitignore for ada support and updates the
Makefile so that it removes the binary on clean.

* Update README and scripts.

Create a temporary README with testing instructions.

Also fix some issues in the debug output of the scripts (the $ was not
escaped properly in some instances).

* Relativize path to anod in run-example

This looks nicer and better supports the common case: in which the user
runs run-example from the repo root.

* Fix python version in Makefile

Makefile was using python to determine the platform; this was one of a
few remaining non-python3 uses of `python`. Having fixed it, things
seem to work smoothly on a machine where python ≠ python3.

* Don't install GNAT CE by default.

Most users won't want to build Ada, so offering to install GNAT CE by
default is likely to just be confusing.

* Change the way Java is installed.

Rather than installing Java (OpenJDK 13) by way of anod in the sandbox,
instead install Java (OpenJDK 11) by way of apt. This results in Java
being available system-wide and avoids having to put ant/java on the
path using anod commands for things like generating LMCP.

Update workflows to install Java using the appropriate github action.
This should reduce the number of spurious build failures we've
encountered.

* Fix run-example issue for uxas-ada.

The shared library for uxas-ada wasn't being placed on the path.
Additionally, there was an unconditional and unlogged exit leftover from
testing in the python script.

* Update anod self-install process to be automatic.

Rather than running the install script in interactive mode, give the
user a full message up front that explains what will happen, followed by
a choice to continue. Then, run the install script in automatic mode.

This avoids some confusion identified whereby the script seems to ask
multiple times to do things in a way that's not particularly helpful
when the expectation is that it will just "take care of things" for the
user.

* Update the README

This new version of the README is tailored to the changes that were made
to integrated -bootstrap into this repository. It is intended to be
minimal and simple. Detail will be provided later to the documentation
site that AFRL is setting up. Once that site is live, links will be made
from this README to that site.

* Improve script with debug_and_run

Rather than printing the string for a command and then separately
issuing the command, we pass the string form of the command to a debug
print method and then eval the string. This removes duplication and
ensures that the printed command really is the command that is executed.

* Minor improvements to README

Fix a couple of typos.
2021-04-01 15:30:51 -04:00
Joffrey Huguet
be3b58d961 Merge pull request #21 from joffreyhuguet/change_reporting_level_in_proof_testsuite
Change report level on proof testsuite
2021-01-25 16:32:37 -05:00
Joffrey Huguet
88a40f522c Update session files and testsuite 2020-12-07 09:50:58 +01:00
Joffrey Huguet
59358ed71a Update session files and testsuite 2020-10-27 13:03:20 +01:00
M. Anthony Aiello
9f7d8f6388 Merge branch 'develop' of https://github.com/afrl-rq/OpenUxAS into integration 2020-09-01 14:26:02 -04:00
Joffrey Huguet
64dc70f749 Merge pull request #8 from joffreyhuguet/add_assignment_tree_branch_bound_service
Add assignment tree branch bound service
2020-09-01 14:18:20 +02:00
Joffrey Huguet
0fec920f63 Update session files 2020-09-01 09:36:35 +02:00
lhumphrey
b57d70211e Adding Example_Spark_Service (#8)
* Example Spark service

* Version 1 of Example_Spark_Service. Minor formatting updates to other Ada files.

* Deleted session files. Added changes to uxas_ada.adb

* Restoring sessions files and adding new session file for example_spark_service
2020-08-26 14:15:09 -04:00
Joffrey Huguet
a1679d6989 Merge pull request #6 from joffreyhuguet/remove_route_aggregator_prefix_in_shared_files
Remove Route_Aggregator_ prefix in SPARK shared files
2020-08-18 17:21:20 +02:00
Joffrey Huguet
098047f90a Remove the Route_Aggregator_ prefix for files that can be shared among several SPARK services 2020-08-18 15:35:33 +02:00
Joffrey Huguet
0a43d70573 Proof testsuite can exit with an error code in case one test fails 2020-08-18 14:56:11 +02:00
M. Anthony Aiello
5c1745313e Final cleanup and refactoring (#57) 2020-07-24 19:13:47 -04:00
M. Anthony Aiello
041d7cc357 Refactor the repository.
This commit makes significant effort towards refactoring the repository
so that it is in a cleaner and more consistent state going forward.

Since we are now explicitly expecting multiple languages to be used for
OpenUxAS, we have reorganized `src` accordingly. Likewise, we have
reorganized `tests`.

This is a candidate for the rebaseline of afrl-rq/OpenUxAS.
2020-07-24 08:39:41 -04:00