Skip to content

When there are ~175k+ .v files, coq_makefile generates a makefile that segfaults make 4.3 #21894

@JasonGross

Description

@JasonGross

Description of the problem

Apparently filter is recursive in make 4.3. A change something like the following seems to do the job

 #                                                                             #
 ###############################################################################

-COQMF_CMDLINE_VFILES :=
-COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES))
-COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES))
-COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES))
-COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES))
-COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES))
-COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES))
-COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES))
+COQMF_CMDLINE_VFILES :=
+_COQMF_SOURCES_CMD = $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES)
+COQMF_SOURCES := $(shell $(_COQMF_SOURCES_CMD) | tr ' ' '\n' > .coqmf_sources.tmp && cat .coqmf_sources.tmp)
+COQMF_VFILES := $(shell grep '\.v$$' .coqmf_sources.tmp)
+COQMF_MLIFILES := $(shell grep '\.mli$$' .coqmf_sources.tmp)
+COQMF_MLFILES := $(shell grep '\.ml$$' .coqmf_sources.tmp)
+COQMF_MLGFILES := $(shell grep '\.mlg$$' .coqmf_sources.tmp)
+COQMF_MLPACKFILES := $(shell grep '\.mlpack$$' .coqmf_sources.tmp)
+COQMF_MLLIBFILES := $(shell grep '\.mllib$$' .coqmf_sources.tmp)
 COQMF_METAFILE =

 ###############################################################################

Note that upgrading to make 4.4 also fixes the issue

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: bugAn error, flaw, fault or unintended behaviour.part: coq_makefileThe coq_makefile binary for generating makefiles.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions