Skip to content

Commit

Permalink
Add idris-start-idris2-project which uses idris2 --init to genera…
Browse files Browse the repository at this point in the history
…te new ipkg file.

Why:
Idris2 does better job to create the ipkg file than us.
  • Loading branch information
keram committed Jul 19, 2024
1 parent 09de86a commit 0d53bf9
Show file tree
Hide file tree
Showing 2 changed files with 154 additions and 0 deletions.
83 changes: 83 additions & 0 deletions idris-commands.el
Original file line number Diff line number Diff line change
Expand Up @@ -1244,6 +1244,89 @@ of the term to replace."
(find-file (car files)))
(t (find-file (completing-read "Package file: " files nil t))))))

(defun idris-start-idris2-project ()
"Interactively create a new Idris2 project with ipkg file and first module."
(interactive)
(cl-flet ((project-name ()
(let ((project-name (string-trim (read-string "Project name: "))))
(when (string-match-p "[^a-zA-Z0-9_ ]" project-name)
(user-error "Project name should consist only of letters, numbers, spaces and underscores"))
(when (string= "" project-name)
(user-error "Project name can not be empty"))
project-name))
(project-directory (default-filename)
(let ((dir (read-directory-name "Create in: " nil default-filename nil default-filename)))
(when (string= "" dir)
(user-error "Project directory can not be empty"))
(when (file-exists-p dir)
(user-error "%s already exists" dir))
dir)))
(let* ((project-name (project-name))
(default-filename (downcase (replace-regexp-in-string "[^a-zA-Z0-9_-]" "-" project-name)))
(package-name default-filename)
(create-in (project-directory default-filename))
(src-dir (string-trim (read-string "Source directory (src): " nil nil "src")))
(authors (string-trim (read-string (format "Authors (%s): " (user-full-name)) nil nil (user-full-name))))
(options (string-trim (read-string "Options: ")))
(module-name-suggestion (replace-regexp-in-string "[^a-zA-Z0-9]+" "." (capitalize project-name)))
(first-mod (string-trim (read-string
(format "First module name (%s): " module-name-suggestion)
nil nil module-name-suggestion)))
(ipkg-file (file-truename (concat (file-name-as-directory create-in)
(concat default-filename ".ipkg"))))
(output-buffer (generate-new-buffer "*Idris Script Output*"))
(input-buffer (generate-new-buffer "*Idris Script Input*")))

(make-directory (concat (file-name-as-directory create-in) src-dir) t)
(with-current-buffer input-buffer
(insert package-name) (newline)
(insert authors) (newline)
(insert options) (newline)
(insert src-dir) (newline)

(call-process-region (point-min) (point-max)
idris-interpreter-path
nil
output-buffer
nil
"--init"
ipkg-file))
(let ((output (with-current-buffer output-buffer
(buffer-string))))
(when (string-match-p "error" output)
(message "Idris: %s" output)))

(kill-buffer output-buffer)
(kill-buffer input-buffer)

;; Decorate the generated ipkg file
(when (file-exists-p ipkg-file)
(save-excursion
(find-file ipkg-file)
(goto-char (point-min))
(insert "-- " project-name) (newline) (newline)
(when (re-search-forward "^-- version =" nil t)
(replace-match "version = 0.1.0"))
(when (and (not (string= first-mod ""))
(re-search-forward "^-- modules =" nil t))
(replace-match "modules = ")
(insert first-mod))
(save-buffer)

;; Create Idris file in the source directory of the project
;; Default directory is the project directry
(when (not (string= first-mod ""))
(let* ((mod-path (reverse (split-string first-mod "\\.+")))
(mod-dir (mapconcat #'file-name-as-directory
(cons src-dir (reverse (cdr mod-path)))
""))
(mod-filename (concat mod-dir (car mod-path) ".idr")))
(make-directory mod-dir t)
(pop-to-buffer (find-file-noselect mod-filename))
(insert "module " first-mod) (newline) (newline)
(insert "%default total") (newline)
(save-buffer))))))))

(defun idris-start-project ()
"Interactively create a new Idris project, complete with ipkg file."
(interactive)
Expand Down
71 changes: 71 additions & 0 deletions test/idris-commands-test.el
Original file line number Diff line number Diff line change
Expand Up @@ -313,6 +313,77 @@ myReverse xs = revAcc [] xs where
(delete-directory mock-directory-name t)
(idris-quit))))

(defmacro idris-generate-mock-read (clauses &optional default)
"Generate a function with cond expression from CLAUSES and optional DEFAULT."
`(lambda (prompt &optional &rest _)
(cond
,@(mapcar (lambda (clause)
`((string-match-p ,(if (symbolp (car clause))
;; Convert symbol to string and
;; remove leading colon and
;; replace dashes with a space
(replace-regexp-in-string
"^\\:" ""
(replace-regexp-in-string "-" " " (symbol-name (car clause))))
(car clause))
prompt)
,(cdr clause)))
clauses)
(t (or ,default "")))))

(ert-deftest idris-start-idris2-project ()
"Test `idris-start-idris2-project' creating a project."

(skip-unless (string-match-p "idris2$" idris-interpreter-path))
(cl-flet ((read-string-stub (idris-generate-mock-read ((:project-name . "Idris2 Test Project")
(:author . "Joe Doe")
(:source-dir . "mysrc")
(:options . "--inc")
(:first-module . "Idris2.Test.Project"))))
(read-dir-stub
(idris-generate-mock-read
((:create-in . (idris-file-name-concat "test-data" "idris2-test-project"))))))
(advice-add 'read-string :override #'read-string-stub)
(advice-add 'read-directory-name :override #'read-dir-stub)
(unwind-protect
(progn
(save-excursion
(idris-start-idris2-project))

(let* ((ipkg-file-path (idris-file-name-concat "test-data"
"idris2-test-project"
"idris2-test-project.ipkg"))
(ipkg-buffer (find-file-noselect ipkg-file-path))
(ipkg-content (with-current-buffer ipkg-buffer
(buffer-substring-no-properties (point-min) (point-max)))))

(should (string-match-p "^-- Idris2 Test Project" ipkg-content))
(should (string-match-p "^package idris2-test-project" ipkg-content))
(should (string-match-p "^version = 0.1.0" ipkg-content))
(should (string-match-p "^authors = \"Joe Doe\"" ipkg-content))
(should (string-match-p "^opts = \"--inc\"" ipkg-content))
(should (string-match-p "^sourcedir = \"mysrc\"" ipkg-content))
(kill-buffer ipkg-buffer))

(let* ((first-mod-file-path (idris-file-name-concat "test-data"
"idris2-test-project"
"mysrc"
"Idris2"
"Test"
"Project.idr"))
(first-mod-buffer (find-file-noselect first-mod-file-path))
(first-mod-content (with-current-buffer first-mod-buffer
(buffer-substring-no-properties (point-min) (point-max)))))

(should (string-match-p "^module Idris2.Test.Project" first-mod-content))
(should (string-match-p "^%default total" first-mod-content))
(kill-buffer first-mod-buffer))

(delete-directory (idris-file-name-concat "test-data" "idris2-test-project") t))

(advice-remove 'read-string #'read-string-stub)
(advice-remove 'read-directory-name #'read-dir-stub))))

;; Tests by Yasuhiko Watanabe
;; https://github.com/idris-hackers/idris-mode/pull/537/files
(idris-ert-command-action "test-data/CaseSplit.idr" idris-case-split idris-test-eq-buffer)
Expand Down

0 comments on commit 0d53bf9

Please sign in to comment.