Using a universal counter means that individual proofs are connected to each other, and changes in one proof affect the other.

We want channel names to be more deterministic and local to a particular proof.

One solution is to add a custom prefix to variable names, one that is unique to the particular proof. This can be:

*processPath*_*stepName*_numberedVariable

For example, when building a composition C1 and composing step _Step1 with counter 5, variable z will be renamed to:

C1__Step1_z5

Note that the step name can be grabbed from the action arguments.

The process path must be provided by the user.

This relies on the following update in the embed library:
PetrosPapapa/hol-light-embed#2

We then need to:

• Add the process path prefix as an action argument or to the action state.
• Update tactics.ml to use the prefix.
• Test test test

The console composer should be extended to enable deployment commands, similarly to how the JSON composer is extended here.

The console does not have a list of commands though. We could either:

1. Maintain a list of deployment commands (similar to the list of actions) or
2. Implement a functor over Composer_console_type.

The deployment output could either be shown in stdout or saved to files locally. A parameter could allow the user to choose between the two.

Some preliminary work here: console.ml

Needs to emulate workspaces, store state, handle processes and compositions, and provide a simple list of commands. Some more pretty printers would also be nice.

Steps to reproduce

loads "workflowfm/src/make.console.ml";;
create "P" [`X`] `A ** A ** A ** A` ;;
create "Q" [`A`;`A`] `Y` ;;
tensor "Q" "Q";;
join "P" "lr" "_Step0" "NEG A";; 

Result

The last command reports the following input provenance:

iprov =
     [(`A ** A ** A ** A`,
       Provnode ("times", Provleaf "cQ_A_1:1",
        Provnode ("times", Provleaf "cQ_A_1:4",
         Provnode ("times", Provleaf "cQ_A_1:8", Provleaf "cQ_A_1:7"))))]

There are only 2x cQ_A_1 channels available, so this input provenance is not possible.

Desired

It should be something along these lines:

iprov =
     [(`A ** A ** A ** A`,
       Provnode ("times", Provleaf "cQ_A_1:1",
        Provnode ("times", Provleaf "cQ_A_2:4",
         Provnode ("times", Provleaf "cQ_A_1:8", Provleaf "cQ_A_2:7"))))]

i.e. 2 of the 4 channels reported should be cQ_A_2 instead of cQ_A_1.

Diagnosis

Something going wrong when tracking unused channels in JOIN_TAC. Need to investigate further.

Currently just outputting a string. It would be nice to have a proper structured json output.

Do we want one generic structure with PiParProc etc. or a different output depending on the process calculus used?

• Change FutureExecutor to ProcessExecutor[_]
• Change executor.context to executor.executionContext
• Change .filterMap(_.map(...)) to .map(...)
• Change default executor (probably to MultiStateExecutor)

Trying to store a composition with the same name as on of its components fails. However, storing it with the same name as one of the component of one of its components succeeds.

Reproduce:

create "P" [`A`] `B`;;
create "Q" [`B`] `C`;;
join "P" "" "Q" "";;
store "_Step1" "R";;
create "S" [`C`] `D`;;
join "R" "" "S" "C";;
store "_Step2" "P";;

Atomic process P gets replaced by a composite process that has R as a component, which in turn has the atomic P as a component. This breaks R as its component P is no longer available. It also creates an undesirable recursive specification.

One could argue this should not be allowed at the level of the logic, but the proof state does not know about components of components, so it allows it.

This will minimize the use of the Actionstate so we won't need to send it back and forth now that the counter does not need to be shared.

Composition commands will only need to provide a context string. The actionstate can be fully constructed with ctr = 0 and the provenance info from the processes.

Tactics will still manipulate provenance in the state because that's the only place they can access it. At the end of the composition, provenance will be extracted back into the composed process.

See ede9a5f

This still does not allow multiple copies of the same
correspondence (though it is not clear why one would ever want this).

When using inference rules, process names (such as "TimesProc") must
be constant. Otherwise they get refreshed with the latest counter like
every other variable (e.g. "TimesProc8").

I feel there is a better way to do this than adding a prefix for each
correspondence, but this will require some rethinking of the embedding
and quite a bit of refactoring.