in cli/src/main/java/org/arend/frontend/BaseCliFrontend.java [319:705]
public CommandLine run(String[] args) {
CommandLine cmdLine = parseArgs(args);
if (cmdLine == null) {
return null;
}
var replKind = cmdLine.getOptionValue("i", "jline");
var defaultLibrariesRoot = FileUtils.defaultLibrariesRoot();
var libDirStrings = cmdLine.hasOption("L")
? cmdLine.getOptionValues("L")
: new String[] { defaultLibrariesRoot.toString() };
// Get library directories
var libDirs = new ArrayList<Path>(libDirStrings.length);
for (String libDirString : libDirStrings) {
var libDir = Paths.get(libDirString);
if (Files.isDirectory(libDir)) {
libDirs.add(libDir);
} else if (!Objects.equals(defaultLibrariesRoot, libDir)) {
myExitWithError = true;
System.err.println("[ERROR] " + libDir + " is not a directory");
}
}
if (cmdLine.hasOption(SHOW_TIMES)) {
myTimes = new HashMap<>();
}
if (cmdLine.hasOption(SHOW_SIZES)) {
mySizes = new HashMap<>();
}
String printString = cmdLine.getOptionValue("p");
if (printString != null) {
Pair<ModulePath, LongName> pair = parseFullName(printString);
myPrintModule = pair.proj1;
myPrintDefinition = pair.proj2;
}
String recompileString = cmdLine.getOptionValue("r");
ModulePath recompileModule = null;
LongName recompileDef = null;
if (recompileString != null) {
Pair<ModulePath, LongName> pair = parseFullName(recompileString);
recompileModule = pair.proj1;
recompileDef = pair.proj2;
}
boolean recompile = recompileString == null && cmdLine.hasOption("r");
if (cmdLine.hasOption("i")) {
switch (replKind.toLowerCase()) {
default:
System.err.println("[ERROR] Unrecognized repl type: " + replKind);
break;
case "plain":
PlainCliRepl.launch(recompile, libDirs);
break;
case "jline":
JLineCliRepl.launch(recompile, libDirs);
break;
}
return null;
}
if (!myLibraryManager.loadLibrary(new PreludeResourceLibrary(), null)) {
return null;
}
myLibraryResolver.addLibraryDirectories(libDirs);
// Get library dependencies
String[] libStrings = cmdLine.getOptionValues("l");
List<LibraryDependency> libraryDependencies = new ArrayList<>();
if (libStrings != null) {
for (String libString : libStrings) {
if (FileUtils.isLibraryName(libString)) {
libraryDependencies.add(new LibraryDependency(libString));
} else {
myExitWithError = true;
System.err.println(LibraryError.illegalName(libString));
}
}
}
// Get source and output directories
String sourceDirStr = cmdLine.getOptionValue("s");
Path sourceDir = sourceDirStr == null ? FileUtils.getCurrentDirectory() : Paths.get(sourceDirStr);
String binaryDirStr = cmdLine.getOptionValue("b");
Path outDir = binaryDirStr != null ? Paths.get(binaryDirStr) : sourceDir.resolve(FileUtils.DEFAULT_BINARIES_DIR);
String extDirStr = cmdLine.getOptionValue("e");
Path extDir = extDirStr != null ? Paths.get(extDirStr) : null;
String extMainClass = cmdLine.getOptionValue("m");
// Collect modules and libraries for which typechecking was requested
Collection<String> argFiles = cmdLine.getArgList();
Set<ModulePath> requestedModules;
List<SourceLibrary> requestedLibraries = new ArrayList<>();
if (argFiles.isEmpty()) {
if (sourceDirStr != null) {
requestedModules = new LinkedHashSet<>();
FileUtils.getModules(sourceDir, FileUtils.EXTENSION, requestedModules, myLibraryManager.getLibraryErrorReporter());
} else {
requestedModules = Collections.emptySet();
}
} else {
requestedModules = new LinkedHashSet<>();
for (String fileName : argFiles) {
Path path = Paths.get(fileName);
boolean isPath = path.isAbsolute() || path.getNameCount() > 1;
if (!Files.exists(path)) {
myLibraryManager.getLibraryErrorReporter().report(new GeneralError(GeneralError.Level.ERROR, "File " + path + " not found"));
} else if (fileName.endsWith(FileUtils.LIBRARY_CONFIG_FILE) || isPath && Files.isDirectory(path)) {
SourceLibrary library = myLibraryResolver.registerLibrary(path.toAbsolutePath().normalize());
if (library != null) {
requestedLibraries.add(library);
}
} else {
ModulePath modulePath;
if (isPath || fileName.endsWith(FileUtils.EXTENSION)) {
modulePath = path.isAbsolute() ? null : FileUtils.modulePath(path, FileUtils.EXTENSION);
} else {
modulePath = FileUtils.modulePath(fileName);
}
if (modulePath == null) {
myLibraryManager.getLibraryErrorReporter().report(FileUtils.illegalModuleName(fileName));
} else {
requestedModules.add(modulePath);
}
}
}
}
if (!requestedModules.isEmpty()) {
try {
Files.createDirectories(outDir);
} catch (IOException e) {
e.printStackTrace();
outDir = null;
}
requestedLibraries.add(new FileSourceLibrary("\\default", sourceDir, outDir, new LibraryHeader(requestedModules, libraryDependencies, null, Range.unbound(), new FileClassLoaderDelegate(extDir), extMainClass), myDependencyCollector));
}
if (requestedLibraries.isEmpty()) {
Path path = Paths.get(FileUtils.LIBRARY_CONFIG_FILE);
if (Files.isRegularFile(path)) {
SourceLibrary library = myLibraryResolver.registerLibrary(path.toAbsolutePath().normalize());
if (library != null) {
requestedLibraries.add(library);
}
} else {
System.out.println("Nothing to load");
return cmdLine;
}
}
// Load and typecheck libraries
MyTypechecking typechecking = new MyTypechecking();
boolean doubleCheck = cmdLine.hasOption("c");
for (SourceLibrary library : requestedLibraries) {
myModuleResults.clear();
if (recompile) {
library.addFlag(SourceLibrary.Flag.RECOMPILE);
}
try {
if (!myLibraryManager.loadLibrary(library, typechecking)) {
continue;
}
} finally {
flushErrors();
}
List<Concrete.Definition> forcedDefs;
if (recompileModule != null) {
List<TCDefReferable> forcedRefs = new ArrayList<>();
if (recompileDef != null) {
Scope scope = library.getModuleScopeProvider().forModule(recompileModule);
if (scope == null && library.loadTests(myLibraryManager, Collections.singletonList(recompileModule))) {
scope = library.getTestsModuleScopeProvider().forModule(recompileModule);
}
if (scope == null) {
System.err.println("[ERROR] Cannot find module '" + recompileModule + "' in library '" + library.getName() + "'");
} else {
Referable ref = Scope.resolveName(scope, recompileDef.toList());
if (!(ref instanceof TCDefReferable)) {
System.err.println("[ERROR] Cannot find definition '" + recompileDef + "' in module '" + recompileModule + "' in library '" + library.getName() + "'");
} else {
forcedRefs.add((TCDefReferable) ref);
}
}
} else {
Group group = library.getModuleGroup(recompileModule, false);
if (group == null && library.loadTests(myLibraryManager, Collections.singletonList(recompileModule))) {
group = library.getModuleGroup(recompileModule, true);
}
if (group == null) {
System.err.println("[ERROR] Cannot find module '" + recompileModule + "' in library '" + library.getName() + "'");
} else {
group.traverseGroup(g -> {
LocatedReferable ref = g.getReferable();
if (ref instanceof TCDefReferable) {
forcedRefs.add((TCDefReferable) ref);
}
});
}
}
forcedDefs = new ArrayList<>();
for (TCDefReferable ref : forcedRefs) {
var def = typechecking.getConcreteProvider().getConcrete(ref);
if (def instanceof Concrete.Definition) {
forcedDefs.add((Concrete.Definition) def);
Definition typechecked = ref.getTypechecked();
ref.setTypechecked(null);
if (typechecked != null) {
for (Definition recursive : typechecked.getRecursiveDefinitions()) {
recursive.getRef().setTypechecked(null);
}
}
}
}
} else {
forcedDefs = null;
}
Collection<? extends ModulePath> modules = library.getUpdatedModules();
int numWithErrors = 0;
if (!modules.isEmpty() || forcedDefs != null) {
System.out.println();
System.out.println("--- Typechecking " + library.getName() + " ---");
long time = System.currentTimeMillis();
try {
if (forcedDefs == null) {
typechecking.typecheckLibrary(library);
} else {
typechecking.typecheckDefinitions(forcedDefs, null);
}
} finally {
time = System.currentTimeMillis() - time;
flushErrors();
// Output nice per-module typechecking results
int numWithGoals = 0;
for (ModulePath module : modules) {
GeneralError.Level result = myModuleResults.get(module);
if (result == null && library.getModuleGroup(module, false) == null && library.getModuleGroup(module, true) == null) {
result = GeneralError.Level.ERROR;
}
reportTypeCheckResult(module, result);
if (result == GeneralError.Level.ERROR) numWithErrors++;
if (result == GeneralError.Level.GOAL) numWithGoals++;
}
if (numWithErrors > 0) {
myExitWithError = true;
System.out.println("Number of modules with errors: " + numWithErrors);
}
if (numWithGoals > 0) {
System.out.println("Number of modules with goals: " + numWithGoals);
}
System.out.println("--- Done (" + timeToString(time) + ") ---");
}
// Persist updated modules
if (library.supportsPersisting()) {
library.persistUpdatedModules(mySystemErrErrorReporter);
}
}
if (myTimes != null && !myTimes.isEmpty()) {
System.out.println();
List<Pair<TCDefReferable,Long>> list = new ArrayList<>(myTimes.size());
for (Map.Entry<TCDefReferable, Pair<Long, Long>> entry : myTimes.entrySet()) {
list.add(new Pair<>(entry.getKey(), entry.getValue().proj2));
}
list.sort((o1, o2) -> Long.compare(o2.proj2, o1.proj2));
for (Pair<TCDefReferable, Long> pair : list) {
System.out.println(pair.proj1.getRefLongName() + ": " + timeToString(pair.proj2));
}
}
if (mySizes != null && !mySizes.isEmpty()) {
System.out.println();
List<Pair<TCDefReferable,Integer>> list = new ArrayList<>(mySizes.size());
for (Map.Entry<TCDefReferable, Integer> entry : mySizes.entrySet()) {
list.add(new Pair<>(entry.getKey(), entry.getValue()));
}
list.sort((o1, o2) -> Long.compare(o2.proj2, o1.proj2));
for (Pair<TCDefReferable, Integer> pair : list) {
System.out.println(pair.proj1.getRefLongName() + ": " + pair.proj2);
}
}
for (Definition definition : myPrintDefinitions) {
System.out.println();
StringBuilder builder = new StringBuilder();
ToAbstractVisitor.convert(definition, PrettyPrinterConfig.DEFAULT).prettyPrint(builder, PrettyPrinterConfig.DEFAULT);
System.out.println(builder);
}
if (cmdLine.hasOption(SHOW_MODULES)) {
System.out.println();
System.out.println("Modules cycles:");
showModules(library, true);
}
if (cmdLine.hasOption(SHOW_MODULES_WITH_INSTANCES)) {
System.out.println();
System.out.println("Modules with instances cycles:");
showModules(library, false);
}
if (doubleCheck && numWithErrors == 0) {
System.out.println();
System.out.println("--- Checking " + library.getName() + " ---");
long time = System.currentTimeMillis();
try {
CoreModuleChecker checker = new CoreModuleChecker(myErrorReporter);
for (ModulePath module : library.getLoadedModules()) {
Group group = library.getModuleGroup(module, false);
if (group != null) {
checker.checkGroup(group);
}
}
} finally {
time = System.currentTimeMillis() - time;
flushErrors();
System.out.println("--- Done (" + timeToString(time) + ") ---");
}
}
}
// Run tests
if (cmdLine.hasOption("t")) {
for (SourceLibrary library : requestedLibraries) {
Collection<? extends ModulePath> modules = library.getTestModules();
if (modules.isEmpty()) {
continue;
}
System.out.println("[INFO] Loading tests for " + library.getName());
long time = System.currentTimeMillis();
boolean loaded = library.loadTests(myLibraryManager);
time = System.currentTimeMillis() - time;
if (!loaded) {
System.out.println("[INFO] Failed loading tests for " + library.getName());
continue;
}
System.out.println("[INFO] Loaded tests for " + library.getName() + " (" + timeToString(time) + ")");
System.out.println();
System.out.println("--- Running tests in " + library.getName() + " ---");
typechecking.clear();
time = System.currentTimeMillis();
try {
typechecking.typecheckTests(library, null);
if (doubleCheck) {
boolean doCheck = true;
for (GeneralError error : myErrorReporter.getErrorList()) {
if (error.level == GeneralError.Level.ERROR) {
doCheck = false;
break;
}
}
if (doCheck) {
CoreModuleChecker checker = new CoreModuleChecker(myErrorReporter);
for (ModulePath module : modules) {
Group group = library.getModuleGroup(module, true);
if (group != null) {
checker.checkGroup(group);
}
}
}
}
} finally {
time = System.currentTimeMillis() - time;
flushErrors();
System.out.println("Tests completed: " + typechecking.total + ", Failed: " + typechecking.failed);
System.out.println("--- Done (" + timeToString(time) + ") ---");
}
}
}
return cmdLine;
}