adding a section to .thm files that contain .mod and .sig

[Dale]

Kaustuv suggested today that Abella's .thm file should have sections
(presumably at the top) that allow .mod and .sig files to be defined.
This would allow a single file (.thm) to contain what is currently in
three files (.sig, .mod, .thm).

This does seem like a nice addition to Abella and might not be hard to
implement. The syntax for the .sig and .mod sections should, of
course, be the same as what they are now.

I told Kaustuv that I would relay his request to this mailing list.
-Dale

[Kaustuv Chaudhuri]

HI guys,

This is really easy to add to Abella. See attached patch and example.

The patch can probably be refactored with a small amount of extra work.

Unfortunately, it confuses the ProofGeneral mode even more than usual.

-- Kaustuv

(PS, sorry for duplicates.)

[Todd Wilson]

I think this would be a useful addition to Abella, as long as it does
not entirely replace the original use of .mod and .sig files. In larger
developments, the modularity one gets by being able to reuse and extend
specification files (with accumulate and accum_sig) is a substantial
benefit.

You may also want to give some thought to how these two specification
methods interact. For example, what if you Import a .thc file that was
compiled from a .thm file that has an inline specification? Can inline
specifications extend .mod/.sig and/or other inline specifications? And
so on.

--Todd

[Andrew Gacek]

Hi,

I think the idea of inline specifications is fine. The concerns Todd
raises about correctness and interactions with other module mechanics
shouldn't be an issue. My concerns are

1. Right now the code isn't refactored and I don't have time to do it.
If I integrate the patch without it, there's a fair chance that
inconsistencies get introduced by later code changes to only one of
the specification mechanisms.

2. The HTML formatter for thm files is fairly dumb and just breaks
things up based on the periods at the end of each command. It would
require a decent amount of work to update it to handle inline
specifications, so I probably won't do that.

-Andrew

> --
> You received this message because you are subscribed to the Google Groups "Abella" group.
> To post to this group, send email to abella-the...@googlegroups.com.
> To unsubscribe from this group, send email to abella-theorem-p...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/abella-theorem-prover?hl=en.
>
>