Greetings! Matt, would it work that when supplying :output-file or defaulting to the input filename, the c, h and data files would all be formed by removing the last ".ext" (if there is one), and then adding ".c" etc.?
Take care, Matt Kaufmann <[email protected]> writes: > Hi, > >> ... I can't see a reason why it >> should use just the smallest suffix (the .tar.gz being a counterexample). > > That's a good point about .tar.gz. So maybe I shouldn't have put this > as a request to modify pathname-name. What I actually would find > helpful is simply for the auxiliary files created by compilation, in > particular the .data file, to have the filename obtained by adding > ".data" after stripping off the ".o" suffix. So in the example I > gave with > :OUTPUT-FILE > <path_to_acl2>/books/projects/aleo/vm/circuits/axe/blake2s1round.old.o > it would be good if the .data file were > <path_to_acl2>/books/projects/aleo/vm/circuits/axe/blake2s1round.old.data > rather than: > <path_to_acl2>/books/projects/aleo/vm/circuits/axe/blake2s1round.data > > If there were a way to specify the .data and .c file in a call of > compile-file, that would be sufficient for my purposes. > > -- Matt > Matthias Buelow <[email protected]> writes: > >> Hi, >> >> I think the main problem here is that Unix-type systems don't really have a >> "file type" in the pathname and therefore the function cannot be implemented >> in >> a naive way like this. For example, what is a .tar.gz file? A gzip file? No, >> it is really a compressed archive and should be treated as such. File >> managers >> often have some sort of table that maps filename suffixes to MIME types, plus >> perhaps some other hardcoded logic, but I think that would be outside of the >> scope of this function. >> >> IMHO there is no proper way to resolve this in a convincing way, I think the >> method gcl has chosen is a legitimate variant and I can't see a reason why it >> should use just the smallest suffix (the .tar.gz being a counterexample). >> >> Best regards >> >> Matthias >> >> >> Am Wed, Nov 19, 2025 at 04:16:34PM -0500 schrieb Camm Maguire: >>> Greetings, and thanks so much for the feedback. >>> >>> It does seem one other user requested this as well. I do not think our >>> behavior violates the spec, but it does vary from other popular >>> implementations. >>> >>> In short, the first '.' terminates the name in GCL. This was convenient >>> in our implementation of pathnames using the regex (e.g. regular >>> expression) engine which has been in GCL for ages. As these follow a >>> left to right algorithm (longest match if I recall), it makes sense to >>> define a terminating character sequence. >>> >>> If interested you can peruse lsp/gcl_make_pathname.lsp, where you will find >>> >>> (defconstant +physical-pathname-defaults+ '(("" "" "" "") >>> ("" "" "" "") >>> ("" "(/?([^/]+/)*)" "" "" "" >>> "([^/]+/)" "/" "/") >>> ("" "([^/.]*)" "" ".") >>> ("." "(\\.[^/]*)?" "" "") >>> ("" "" "" ""))) >>> >>> and an analog for logical pathnames that govern the parsing. I can >>> describe the role of each string in the group if interested. >>> >>> I will try to look at the already implemented regex engine to see if a >>> negative look-ahead could be supported. >>> >>> Take care, >>> >>> >>> Matt Kaufmann <[email protected]> writes: >>> >>> > Hi Camm, >>> > >>> > Here's a request: Could you arrange that for any file with a name of the >>> > form "<name>.lisp", then its pathname-name is "<name>" and its >>> > pathname-type is "lisp"? This is not always the case, at least in my >>> > version of GCL 2.7.1, when "<name>" contains a dot (i.e., character >>> > #\.). >>> > >>> > Below I explain further what I'm seeing and why this is a problem for >>> > ACL2. (Probably one can imagine a similar problem for other systems.) >>> > >>> > Here is behavior I'm seeing in GCL 2.7.1, which causes a problem for >>> > ACL2 as explained below. >>> > >>> >>(pathname-name (pathname "foo.xyz.lisp")) >>> > >>> > "foo" >>> > >>> >>(pathname-name "foo.xyz.lisp") >>> > >>> > "foo" >>> > >>> >>(pathname-type (pathname "foo.xyz.lisp")) >>> > >>> > "xyz.lisp" >>> > >>> >>(pathname-type "foo.xyz.lisp") >>> > >>> > "xyz.lisp" >>> > >>> >> >>> > >>> > I'd prefer to see the behavior shown in the following example, i.e., >>> > returning a pathname-type of "lisp". >>> > >>> >>(pathname-name "foo-xyz.lisp") >>> > >>> > "foo-xyz" >>> > >>> >>(pathname-type "foo-xyz.lisp") >>> > >>> > "lisp" >>> > >>> >> >>> > >>> > I'm not sure this behavior is in error, by the way -- just surprising >>> > (to me) and, in the case of ACL2, inconvenient. Here's what I found >>> > in the CL HyperSPec. >>> > >>> > https://www.lispworks.com/documentation/HyperSpec/Body/19_bae.htm >>> > >>> > 19.2.1.5 The Pathname Type Component >>> > >>> > Corresponds to the ``filetype'' or ``extension'' concept in many >>> > host file systems. This says what kind of file this is. This >>> > component is always a string, nil, :wild, or :unspecific. >>> > >>> > To me, it is natural to view "foo.xyz.lisp" as a lisp file, hence with >>> > extension "lisp" to say that the "kind of file" is a lisp file. >>> > >>> > This gets in the way for ACL2 in the case of the following two books. >>> > >>> > books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp >>> > books/projects/aleo/vm/circuits/axe/blake2s1round.lisp >>> > >>> > When we do certifications in parallel (i.e., with -j greater than 1), >>> > compilation can be attempted in parallel. The two books above can >>> > thus lead to the following calls done by two GCL processes in >>> > parallel. >>> > >>> > (COMPILE-FILE >>> > >>> > "<path_to_acl2>/books/projects/aleo/vm/circuits/axe/[email protected]" >>> > :OUTPUT-FILE >>> > "<path_to_acl2>/books/projects/aleo/vm/circuits/axe/blake2s1round.old.o") >>> > >>> > (COMPILE-FILE >>> > "<path_to_acl2>/books/projects/aleo/vm/circuits/axe/blake2s1round.lsp" >>> > :OUTPUT-FILE >>> > "<path_to_acl2>/books/projects/aleo/vm/circuits/axe/blake2s1round.o") >>> > >>> > Both of these compilations attempt to create the same file, >>> > "<path_to_acl2>/books/projects/aleo/vm/circuits/axe/blake2s1round.data". >>> > I suspect that if pathname-name were changed as described above, then >>> > the first compile-file call above would instead create >>> > "<path_to_acl2>/books/projects/aleo/vm/circuits/axe/blake2s1round.old.data". >>> > >>> > Thanks, >>> > Matt >>> > >>> >>> -- >>> Camm Maguire >>> [email protected] >>> ========================================================================== >>> "The earth is but one country, and mankind its citizens." -- Baha'u'llah >>> > > > > -- Camm Maguire [email protected] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah
