Hi Camm, Yes, that would be great!
Thanks, Matt Camm Maguire <[email protected]> writes: > 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
